------------------------------------------------------------
Building: 0
------------------------------------------------------------
	---;	l9,cond;	---;	l4;
	l7;	---;	l5;	l2;
	---;	l8;	l6,cond;	---;
	l1,cond;	l0,cond;	---;	l3;
INDEX: 0
OrderedPatrolling([r in l1, r in l2]),	UpperRestrictedAvoidance(r in l3,2),	Wait(cond,r in l4)

( ( ( ( AG (AF (( ( state = l1)) & (AF (( state = l2)) )))) & (( TRUE) & (A[ (  ! (( state = l2))) U (( state = l1) ) ] ) )) & (( AG (( ( state = l2)) -> (AX (A[ (  ! (( state = l2))) U (( state = l1) ) ]) ))) & (AG (( ( state = l2)) -> (AX (A[ (  ! (( state = l2))) U (( state = l1) ) ]) )) ) )) & ( ! (AF (( ( state = l3)) & (AX (AF (( ( state = l3)) & (AX (AF (( ( state = l3)) & (AX (AF (( state = l3))) ))) ))) ))) )) & (A[ ( (cond)) U (( state = l4) ) ] )
( ( ( (  G ( F (( (l1)) & ( F ((l2)) )))) & ((  ! ((l2))) U ((l1) ) )) & ((  G (( (l2)) -> ( X ((  ! ((l2))) U ((l1) )) ))) & ( G (( (l2)) -> ( X ((  ! ((l2))) U ((l1) )) )) ) )) & ( ! ( F (( (l3)) & ( X ( F (( (l3)) & ( X ( F (( (l3)) & ( X ( F ((l3))) ))) ))) ))) )) & (( (cond)) U ((l4) ) )
NuSMV/LTLmodel_0_0.smv
NuSMV/CTLmodel_0_0.smv
LTL: true
CTL: true
INDEX: 1
FairVisit([r in l1, r in l2]),	NO,	DelayedReaction(cond,r exec act)

( ( ( AF (( state = l1))) & (AF (( state = l2)) )) & (( AG (( ( state = l1)) -> (AX ( ! (E[ ( (  ! (( state = l1))) & ( ! (( state = l2)) )) U ((  ! ( ! (( state = l1)))) & ( ! (( state = l2)) ) ) ])) ))) & (AG (( ( state = l2)) -> (AX ( ! (E[ ( (  ! (( state = l2))) & ( ! (( state = l1)) )) U ((  ! ( ! (( state = l2)))) & ( ! (( state = l1)) ) ) ])) )) ) )) & (AG (( (cond)) -> (AF ((act)) )) )
( ( ( (  F ((l1))) & ( F ((l2)) )) & ((  G (( (l1)) -> ( X (((  ! ((l1))) U ((l2) ) | ( G ( ! ((l1))) ) )) ))) & ( G (( (l2)) -> ( X (((  ! ((l2))) U ((l1) ) | ( G ( ! ((l2))) ) )) )) ) )) & (TRUE )) & ( G (( (cond)) -> ( F ((act)) )) )
NuSMV/LTLmodel_0_1.smv
NuSMV/CTLmodel_0_1.smv
LTL: true
CTL: true
INDEX: 2
StrictOrderedVisit([r in l1, r in l2]),	GlobalAvoidance(r in l3),	InstantaneousReaction(cond,r exec act)

( ( ( ( AF (( ( state = l1)) & (AF (( state = l2)) ))) & (A[ (  ! (( state = l2))) U (( state = l1) ) ] )) & (A[ (  ! (( state = l1))) U (( ( state = l1)) & (AX (A[ (  ! (( state = l1))) U (( state = l2) ) ]) ) ) ] )) & (AG ( ! (( state = l3))) )) & (AG (( (cond)) -> ((act) )) )
( ( ( (  F (( (l1)) & ( F ((l2)) ))) & ((  ! ((l2))) U ((l1) ) )) & ((  ! ((l1))) U (( (l1)) & ( X ((  ! ((l1))) U ((l2) )) ) ) )) & ( G ( ! ((l3))) )) & ( G (( (cond)) -> ((act) )) )
NuSMV/LTLmodel_0_2.smv
NuSMV/CTLmodel_0_2.smv
LTL: false
CTL: false
INDEX: 3
SequencedVisit([r in l1, r in l2]),	FutureAvoidance(cond,r in l3),	NO,	
( AF (( ( state = l1)) & (AF (( state = l2)) ))) & (AG (( (cond)) -> (AG ( ! (( state = l3))) )) )
( (  F (( (l1)) & ( F ((l2)) ))) & ( G (( (cond)) -> ( G ( ! ((l3))) )) )) & (TRUE )
NuSMV/LTLmodel_0_3.smv
NuSMV/CTLmodel_0_3.smv
LTL: true
CTL: true
INDEX: 4
OrderedVisit([r in l1, r in l2]),	PastAvoidance(cond,r in l3),	InstantaneousReaction(cond,r exec act)

( ( ( AF (( ( state = l1)) & (AF (( state = l2)) ))) & (A[ (  ! (( state = l2))) U (( state = l1) ) ] )) & (A[ (  ! (( state = l3))) U ((cond) ) ] )) & (AG (( (cond)) -> ((act) )) )
( ( (  F (( (l1)) & ( F ((l2)) ))) & ((  ! ((l2))) U ((l1) ) )) & ((  ! ((l3))) U ((cond) ) )) & ( G (( (cond)) -> ((act) )) )
NuSMV/LTLmodel_0_4.smv
NuSMV/CTLmodel_0_4.smv
LTL: false
CTL: false
INDEX: 5
Visit([r in l1, r in l2]),	LowerRestrictedAvoidance(r in l3,2),	BindedReaction(cond,r exec act)

( ( ( AF (( state = l1))) & (AF (( state = l2)) )) & (AF (( ( state = l3)) & (AX (AF (( state = l3))) )) )) & (AG (( (cond)) <-> ((act) )) )
( ( (  F ((l1))) & ( F ((l2)) )) & ( F (( (l3)) & ( X ( F ((l3))) )) )) & ( G (( (cond)) <-> ((act) )) )
NuSMV/LTLmodel_0_5.smv
NuSMV/CTLmodel_0_5.smv
LTL: false
CTL: false
INDEX: 6
StrictOrderedPatrolling([r in l1, r in l2]),	FutureAvoidance(cond,r in l3),	Wait(cond,r in l4)

( ( ( ( ( AG (AF (( ( state = l1)) & (AF (( state = l2)) )))) & (( TRUE) & (A[ (  ! (( state = l2))) U (( state = l1) ) ] ) )) & (( AG (( ( state = l2)) -> (AX (A[ (  ! (( state = l2))) U (( state = l1) ) ]) ))) & (AG (( ( state = l2)) -> (AX (A[ (  ! (( state = l2))) U (( state = l1) ) ]) )) ) )) & (( AG (( ( state = l1)) -> (AX (A[ (  ! (( state = l1))) U (( state = l2) ) ]) ))) & (AG (( ( state = l2)) -> (AX (A[ (  ! (( state = l2))) U (( state = l1) ) ]) )) ) )) & (AG (( (cond)) -> (AG ( ! (( state = l3))) )) )) & (A[ ( (cond)) U (( state = l4) ) ] )
( ( ( ( (  G ( F (( (l1)) & ( F ((l2)) )))) & ((  ! ((l2))) U ((l1) ) )) & ((  G (( (l2)) -> ( X ((  ! ((l2))) U ((l1) )) ))) & ( G (( (l2)) -> ( X ((  ! ((l2))) U ((l1) )) )) ) )) & ((  G (( (l1)) -> ( X ((  ! ((l1))) U ((l2) )) ))) & ( G (( (l2)) -> ( X ((  ! ((l2))) U ((l1) )) )) ) )) & ( G (( (cond)) -> ( G ( ! ((l3))) )) )) & (( (cond)) U ((l4) ) )
NuSMV/LTLmodel_0_6.smv
NuSMV/CTLmodel_0_6.smv
LTL: true
CTL: true
INDEX: 7
Patrolling([r in l1, r in l2]),	LowerRestrictedAvoidance(r in l3,2),	InstantaneousReaction(cond,r exec act)

( ( AG (( ( TRUE) & (AF (( state = l1)) )) & (AF (( state = l2)) ))) & (AF (( ( state = l3)) & (AX (AF (( state = l3))) )) )) & (AG (( (cond)) -> ((act) )) )
( (  G ((  F ((l1))) & ( F ((l2)) ))) & ( F (( (l3)) & ( X ( F ((l3))) )) )) & ( G (( (cond)) -> ((act) )) )
NuSMV/LTLmodel_0_7.smv
NuSMV/CTLmodel_0_7.smv
LTL: false
CTL: false
INDEX: 8
FairPatrolling([r in l1, r in l2]),	NO,	DelayedReaction(cond,r exec act)

( ( AG (( AF (( state = l1))) & (AF (( state = l2)) ))) & (( AG (( ( state = l1)) -> (AX ( ! (E[ ( (  ! (( state = l1))) & ( ! (( state = l2)) )) U ((  ! ( ! (( state = l1)))) & ( ! (( state = l2)) ) ) ])) ))) & (AG (( ( state = l2)) -> (AX ( ! (E[ ( (  ! (( state = l2))) & ( ! (( state = l1)) )) U ((  ! ( ! (( state = l2)))) & ( ! (( state = l1)) ) ) ])) )) ) )) & (AG (( (cond)) -> (AF ((act)) )) )
( ( (  G ((  F ((l1))) & ( F ((l2)) ))) & ((  G (( (l1)) -> ( X (((  ! ((l1))) U ((l2) ) | ( G ( ! ((l1))) ) )) ))) & ( G (( (l2)) -> ( X (((  ! ((l2))) U ((l1) ) | ( G ( ! ((l2))) ) )) )) ) )) & (TRUE )) & ( G (( (cond)) -> ( F ((act)) )) )
NuSMV/LTLmodel_0_8.smv
NuSMV/CTLmodel_0_8.smv
LTL: true
CTL: true
INDEX: 9
SequencedPatrolling([r in l1, r in l2]),	UpperRestrictedAvoidance(r in l3,2),	NO,	
( AG (AF (( ( state = l1)) & (AF (( state = l2)) )))) & ( ! (AF (( ( state = l3)) & (AX (AF (( ( state = l3)) & (AX (AF (( ( state = l3)) & (AX (AF (( state = l3))) ))) ))) ))) )
( (  G ( F (( (l1)) & ( F ((l2)) )))) & ( ! ( F (( (l3)) & ( X ( F (( (l3)) & ( X ( F (( (l3)) & ( X ( F ((l3))) ))) ))) ))) )) & (TRUE )
NuSMV/LTLmodel_0_9.smv
NuSMV/CTLmodel_0_9.smv
LTL: true
CTL: true
------------------------------------------------------------
Building: 1
------------------------------------------------------------
	---;	l3;	l8;	---;
	l6;	l2,cond;	---;	l5;
	l9;	l4,cond;	---;	l7;
	l1,cond;	l0,cond;	---;	---;
INDEX: 0
OrderedPatrolling([r in l1, r in l2]),	UpperRestrictedAvoidance(r in l3,2),	Wait(cond,r in l4)

( ( ( ( AG (AF (( ( state = l1)) & (AF (( state = l2)) )))) & (( TRUE) & (A[ (  ! (( state = l2))) U (( state = l1) ) ] ) )) & (( AG (( ( state = l2)) -> (AX (A[ (  ! (( state = l2))) U (( state = l1) ) ]) ))) & (AG (( ( state = l2)) -> (AX (A[ (  ! (( state = l2))) U (( state = l1) ) ]) )) ) )) & ( ! (AF (( ( state = l3)) & (AX (AF (( ( state = l3)) & (AX (AF (( ( state = l3)) & (AX (AF (( state = l3))) ))) ))) ))) )) & (A[ ( (cond)) U (( state = l4) ) ] )
( ( ( (  G ( F (( (l1)) & ( F ((l2)) )))) & ((  ! ((l2))) U ((l1) ) )) & ((  G (( (l2)) -> ( X ((  ! ((l2))) U ((l1) )) ))) & ( G (( (l2)) -> ( X ((  ! ((l2))) U ((l1) )) )) ) )) & ( ! ( F (( (l3)) & ( X ( F (( (l3)) & ( X ( F (( (l3)) & ( X ( F ((l3))) ))) ))) ))) )) & (( (cond)) U ((l4) ) )
NuSMV/LTLmodel_1_0.smv
NuSMV/CTLmodel_1_0.smv
LTL: false
CTL: false
INDEX: 1
FairVisit([r in l1, r in l2]),	NO,	DelayedReaction(cond,r exec act)

( ( ( AF (( state = l1))) & (AF (( state = l2)) )) & (( AG (( ( state = l1)) -> (AX ( ! (E[ ( (  ! (( state = l1))) & ( ! (( state = l2)) )) U ((  ! ( ! (( state = l1)))) & ( ! (( state = l2)) ) ) ])) ))) & (AG (( ( state = l2)) -> (AX ( ! (E[ ( (  ! (( state = l2))) & ( ! (( state = l1)) )) U ((  ! ( ! (( state = l2)))) & ( ! (( state = l1)) ) ) ])) )) ) )) & (AG (( (cond)) -> (AF ((act)) )) )
( ( ( (  F ((l1))) & ( F ((l2)) )) & ((  G (( (l1)) -> ( X (((  ! ((l1))) U ((l2) ) | ( G ( ! ((l1))) ) )) ))) & ( G (( (l2)) -> ( X (((  ! ((l2))) U ((l1) ) | ( G ( ! ((l2))) ) )) )) ) )) & (TRUE )) & ( G (( (cond)) -> ( F ((act)) )) )
NuSMV/LTLmodel_1_1.smv
NuSMV/CTLmodel_1_1.smv
LTL: true
CTL: true
INDEX: 2
StrictOrderedVisit([r in l1, r in l2]),	GlobalAvoidance(r in l3),	InstantaneousReaction(cond,r exec act)

( ( ( ( AF (( ( state = l1)) & (AF (( state = l2)) ))) & (A[ (  ! (( state = l2))) U (( state = l1) ) ] )) & (A[ (  ! (( state = l1))) U (( ( state = l1)) & (AX (A[ (  ! (( state = l1))) U (( state = l2) ) ]) ) ) ] )) & (AG ( ! (( state = l3))) )) & (AG (( (cond)) -> ((act) )) )
( ( ( (  F (( (l1)) & ( F ((l2)) ))) & ((  ! ((l2))) U ((l1) ) )) & ((  ! ((l1))) U (( (l1)) & ( X ((  ! ((l1))) U ((l2) )) ) ) )) & ( G ( ! ((l3))) )) & ( G (( (cond)) -> ((act) )) )
NuSMV/LTLmodel_1_2.smv
NuSMV/CTLmodel_1_2.smv
LTL: false
CTL: false
INDEX: 3
SequencedVisit([r in l1, r in l2]),	FutureAvoidance(cond,r in l3),	NO,	
( AF (( ( state = l1)) & (AF (( state = l2)) ))) & (AG (( (cond)) -> (AG ( ! (( state = l3))) )) )
( (  F (( (l1)) & ( F ((l2)) ))) & ( G (( (cond)) -> ( G ( ! ((l3))) )) )) & (TRUE )
NuSMV/LTLmodel_1_3.smv
NuSMV/CTLmodel_1_3.smv
LTL: false
CTL: false
INDEX: 4
OrderedVisit([r in l1, r in l2]),	PastAvoidance(cond,r in l3),	InstantaneousReaction(cond,r exec act)

( ( ( AF (( ( state = l1)) & (AF (( state = l2)) ))) & (A[ (  ! (( state = l2))) U (( state = l1) ) ] )) & (A[ (  ! (( state = l3))) U ((cond) ) ] )) & (AG (( (cond)) -> ((act) )) )
( ( (  F (( (l1)) & ( F ((l2)) ))) & ((  ! ((l2))) U ((l1) ) )) & ((  ! ((l3))) U ((cond) ) )) & ( G (( (cond)) -> ((act) )) )
NuSMV/LTLmodel_1_4.smv
NuSMV/CTLmodel_1_4.smv
LTL: false
CTL: false
INDEX: 5
Visit([r in l1, r in l2]),	LowerRestrictedAvoidance(r in l3,2),	BindedReaction(cond,r exec act)

( ( ( AF (( state = l1))) & (AF (( state = l2)) )) & (AF (( ( state = l3)) & (AX (AF (( state = l3))) )) )) & (AG (( (cond)) <-> ((act) )) )
( ( (  F ((l1))) & ( F ((l2)) )) & ( F (( (l3)) & ( X ( F ((l3))) )) )) & ( G (( (cond)) <-> ((act) )) )
NuSMV/LTLmodel_1_5.smv
NuSMV/CTLmodel_1_5.smv
LTL: false
CTL: false
INDEX: 6
StrictOrderedPatrolling([r in l1, r in l2]),	FutureAvoidance(cond,r in l3),	Wait(cond,r in l4)

( ( ( ( ( AG (AF (( ( state = l1)) & (AF (( state = l2)) )))) & (( TRUE) & (A[ (  ! (( state = l2))) U (( state = l1) ) ] ) )) & (( AG (( ( state = l2)) -> (AX (A[ (  ! (( state = l2))) U (( state = l1) ) ]) ))) & (AG (( ( state = l2)) -> (AX (A[ (  ! (( state = l2))) U (( state = l1) ) ]) )) ) )) & (( AG (( ( state = l1)) -> (AX (A[ (  ! (( state = l1))) U (( state = l2) ) ]) ))) & (AG (( ( state = l2)) -> (AX (A[ (  ! (( state = l2))) U (( state = l1) ) ]) )) ) )) & (AG (( (cond)) -> (AG ( ! (( state = l3))) )) )) & (A[ ( (cond)) U (( state = l4) ) ] )
( ( ( ( (  G ( F (( (l1)) & ( F ((l2)) )))) & ((  ! ((l2))) U ((l1) ) )) & ((  G (( (l2)) -> ( X ((  ! ((l2))) U ((l1) )) ))) & ( G (( (l2)) -> ( X ((  ! ((l2))) U ((l1) )) )) ) )) & ((  G (( (l1)) -> ( X ((  ! ((l1))) U ((l2) )) ))) & ( G (( (l2)) -> ( X ((  ! ((l2))) U ((l1) )) )) ) )) & ( G (( (cond)) -> ( G ( ! ((l3))) )) )) & (( (cond)) U ((l4) ) )
NuSMV/LTLmodel_1_6.smv
NuSMV/CTLmodel_1_6.smv
LTL: false
CTL: false
INDEX: 7
Patrolling([r in l1, r in l2]),	LowerRestrictedAvoidance(r in l3,2),	InstantaneousReaction(cond,r exec act)

( ( AG (( ( TRUE) & (AF (( state = l1)) )) & (AF (( state = l2)) ))) & (AF (( ( state = l3)) & (AX (AF (( state = l3))) )) )) & (AG (( (cond)) -> ((act) )) )
( (  G ((  F ((l1))) & ( F ((l2)) ))) & ( F (( (l3)) & ( X ( F ((l3))) )) )) & ( G (( (cond)) -> ((act) )) )
NuSMV/LTLmodel_1_7.smv
NuSMV/CTLmodel_1_7.smv
LTL: false
CTL: false
INDEX: 8
FairPatrolling([r in l1, r in l2]),	NO,	DelayedReaction(cond,r exec act)

( ( AG (( AF (( state = l1))) & (AF (( state = l2)) ))) & (( AG (( ( state = l1)) -> (AX ( ! (E[ ( (  ! (( state = l1))) & ( ! (( state = l2)) )) U ((  ! ( ! (( state = l1)))) & ( ! (( state = l2)) ) ) ])) ))) & (AG (( ( state = l2)) -> (AX ( ! (E[ ( (  ! (( state = l2))) & ( ! (( state = l1)) )) U ((  ! ( ! (( state = l2)))) & ( ! (( state = l1)) ) ) ])) )) ) )) & (AG (( (cond)) -> (AF ((act)) )) )
( ( (  G ((  F ((l1))) & ( F ((l2)) ))) & ((  G (( (l1)) -> ( X (((  ! ((l1))) U ((l2) ) | ( G ( ! ((l1))) ) )) ))) & ( G (( (l2)) -> ( X (((  ! ((l2))) U ((l1) ) | ( G ( ! ((l2))) ) )) )) ) )) & (TRUE )) & ( G (( (cond)) -> ( F ((act)) )) )
NuSMV/LTLmodel_1_8.smv
NuSMV/CTLmodel_1_8.smv
LTL: true
CTL: true
INDEX: 9
SequencedPatrolling([r in l1, r in l2]),	UpperRestrictedAvoidance(r in l3,2),	NO,	
( AG (AF (( ( state = l1)) & (AF (( state = l2)) )))) & ( ! (AF (( ( state = l3)) & (AX (AF (( ( state = l3)) & (AX (AF (( ( state = l3)) & (AX (AF (( state = l3))) ))) ))) ))) )
( (  G ( F (( (l1)) & ( F ((l2)) )))) & ( ! ( F (( (l3)) & ( X ( F (( (l3)) & ( X ( F (( (l3)) & ( X ( F ((l3))) ))) ))) ))) )) & (TRUE )
NuSMV/LTLmodel_1_9.smv
NuSMV/CTLmodel_1_9.smv
LTL: false
CTL: false
------------------------------------------------------------
Building: 2
------------------------------------------------------------
	l9,cond;	---;	l6,cond;	l5;
	---;	l4;	---;	l2,cond;
	---;	l7,cond;	l0;	l1;
	l8;	---;	l3;	---;
INDEX: 0
OrderedPatrolling([r in l1, r in l2]),	UpperRestrictedAvoidance(r in l3,2),	Wait(cond,r in l4)

( ( ( ( AG (AF (( ( state = l1)) & (AF (( state = l2)) )))) & (( TRUE) & (A[ (  ! (( state = l2))) U (( state = l1) ) ] ) )) & (( AG (( ( state = l2)) -> (AX (A[ (  ! (( state = l2))) U (( state = l1) ) ]) ))) & (AG (( ( state = l2)) -> (AX (A[ (  ! (( state = l2))) U (( state = l1) ) ]) )) ) )) & ( ! (AF (( ( state = l3)) & (AX (AF (( ( state = l3)) & (AX (AF (( ( state = l3)) & (AX (AF (( state = l3))) ))) ))) ))) )) & (A[ ( (cond)) U (( state = l4) ) ] )
( ( ( (  G ( F (( (l1)) & ( F ((l2)) )))) & ((  ! ((l2))) U ((l1) ) )) & ((  G (( (l2)) -> ( X ((  ! ((l2))) U ((l1) )) ))) & ( G (( (l2)) -> ( X ((  ! ((l2))) U ((l1) )) )) ) )) & ( ! ( F (( (l3)) & ( X ( F (( (l3)) & ( X ( F (( (l3)) & ( X ( F ((l3))) ))) ))) ))) )) & (( (cond)) U ((l4) ) )
NuSMV/LTLmodel_2_0.smv
NuSMV/CTLmodel_2_0.smv
LTL: false
CTL: false
INDEX: 1
FairVisit([r in l1, r in l2]),	NO,	DelayedReaction(cond,r exec act)

( ( ( AF (( state = l1))) & (AF (( state = l2)) )) & (( AG (( ( state = l1)) -> (AX ( ! (E[ ( (  ! (( state = l1))) & ( ! (( state = l2)) )) U ((  ! ( ! (( state = l1)))) & ( ! (( state = l2)) ) ) ])) ))) & (AG (( ( state = l2)) -> (AX ( ! (E[ ( (  ! (( state = l2))) & ( ! (( state = l1)) )) U ((  ! ( ! (( state = l2)))) & ( ! (( state = l1)) ) ) ])) )) ) )) & (AG (( (cond)) -> (AF ((act)) )) )
( ( ( (  F ((l1))) & ( F ((l2)) )) & ((  G (( (l1)) -> ( X (((  ! ((l1))) U ((l2) ) | ( G ( ! ((l1))) ) )) ))) & ( G (( (l2)) -> ( X (((  ! ((l2))) U ((l1) ) | ( G ( ! ((l2))) ) )) )) ) )) & (TRUE )) & ( G (( (cond)) -> ( F ((act)) )) )
NuSMV/LTLmodel_2_1.smv
NuSMV/CTLmodel_2_1.smv
LTL: false
CTL: false
INDEX: 2
StrictOrderedVisit([r in l1, r in l2]),	GlobalAvoidance(r in l3),	InstantaneousReaction(cond,r exec act)

( ( ( ( AF (( ( state = l1)) & (AF (( state = l2)) ))) & (A[ (  ! (( state = l2))) U (( state = l1) ) ] )) & (A[ (  ! (( state = l1))) U (( ( state = l1)) & (AX (A[ (  ! (( state = l1))) U (( state = l2) ) ]) ) ) ] )) & (AG ( ! (( state = l3))) )) & (AG (( (cond)) -> ((act) )) )
( ( ( (  F (( (l1)) & ( F ((l2)) ))) & ((  ! ((l2))) U ((l1) ) )) & ((  ! ((l1))) U (( (l1)) & ( X ((  ! ((l1))) U ((l2) )) ) ) )) & ( G ( ! ((l3))) )) & ( G (( (cond)) -> ((act) )) )
NuSMV/LTLmodel_2_2.smv
NuSMV/CTLmodel_2_2.smv
LTL: false
CTL: false
INDEX: 3
SequencedVisit([r in l1, r in l2]),	FutureAvoidance(cond,r in l3),	NO,	
( AF (( ( state = l1)) & (AF (( state = l2)) ))) & (AG (( (cond)) -> (AG ( ! (( state = l3))) )) )
( (  F (( (l1)) & ( F ((l2)) ))) & ( G (( (cond)) -> ( G ( ! ((l3))) )) )) & (TRUE )
NuSMV/LTLmodel_2_3.smv
NuSMV/CTLmodel_2_3.smv
LTL: false
CTL: false
INDEX: 4
OrderedVisit([r in l1, r in l2]),	PastAvoidance(cond,r in l3),	InstantaneousReaction(cond,r exec act)

( ( ( AF (( ( state = l1)) & (AF (( state = l2)) ))) & (A[ (  ! (( state = l2))) U (( state = l1) ) ] )) & (A[ (  ! (( state = l3))) U ((cond) ) ] )) & (AG (( (cond)) -> ((act) )) )
( ( (  F (( (l1)) & ( F ((l2)) ))) & ((  ! ((l2))) U ((l1) ) )) & ((  ! ((l3))) U ((cond) ) )) & ( G (( (cond)) -> ((act) )) )
NuSMV/LTLmodel_2_4.smv
NuSMV/CTLmodel_2_4.smv
LTL: false
CTL: false
INDEX: 5
Visit([r in l1, r in l2]),	LowerRestrictedAvoidance(r in l3,2),	BindedReaction(cond,r exec act)

( ( ( AF (( state = l1))) & (AF (( state = l2)) )) & (AF (( ( state = l3)) & (AX (AF (( state = l3))) )) )) & (AG (( (cond)) <-> ((act) )) )
( ( (  F ((l1))) & ( F ((l2)) )) & ( F (( (l3)) & ( X ( F ((l3))) )) )) & ( G (( (cond)) <-> ((act) )) )
NuSMV/LTLmodel_2_5.smv
NuSMV/CTLmodel_2_5.smv
LTL: false
CTL: false
INDEX: 6
StrictOrderedPatrolling([r in l1, r in l2]),	FutureAvoidance(cond,r in l3),	Wait(cond,r in l4)

( ( ( ( ( AG (AF (( ( state = l1)) & (AF (( state = l2)) )))) & (( TRUE) & (A[ (  ! (( state = l2))) U (( state = l1) ) ] ) )) & (( AG (( ( state = l2)) -> (AX (A[ (  ! (( state = l2))) U (( state = l1) ) ]) ))) & (AG (( ( state = l2)) -> (AX (A[ (  ! (( state = l2))) U (( state = l1) ) ]) )) ) )) & (( AG (( ( state = l1)) -> (AX (A[ (  ! (( state = l1))) U (( state = l2) ) ]) ))) & (AG (( ( state = l2)) -> (AX (A[ (  ! (( state = l2))) U (( state = l1) ) ]) )) ) )) & (AG (( (cond)) -> (AG ( ! (( state = l3))) )) )) & (A[ ( (cond)) U (( state = l4) ) ] )
( ( ( ( (  G ( F (( (l1)) & ( F ((l2)) )))) & ((  ! ((l2))) U ((l1) ) )) & ((  G (( (l2)) -> ( X ((  ! ((l2))) U ((l1) )) ))) & ( G (( (l2)) -> ( X ((  ! ((l2))) U ((l1) )) )) ) )) & ((  G (( (l1)) -> ( X ((  ! ((l1))) U ((l2) )) ))) & ( G (( (l2)) -> ( X ((  ! ((l2))) U ((l1) )) )) ) )) & ( G (( (cond)) -> ( G ( ! ((l3))) )) )) & (( (cond)) U ((l4) ) )
NuSMV/LTLmodel_2_6.smv
NuSMV/CTLmodel_2_6.smv
LTL: false
CTL: false
INDEX: 7
Patrolling([r in l1, r in l2]),	LowerRestrictedAvoidance(r in l3,2),	InstantaneousReaction(cond,r exec act)

( ( AG (( ( TRUE) & (AF (( state = l1)) )) & (AF (( state = l2)) ))) & (AF (( ( state = l3)) & (AX (AF (( state = l3))) )) )) & (AG (( (cond)) -> ((act) )) )
( (  G ((  F ((l1))) & ( F ((l2)) ))) & ( F (( (l3)) & ( X ( F ((l3))) )) )) & ( G (( (cond)) -> ((act) )) )
NuSMV/LTLmodel_2_7.smv
NuSMV/CTLmodel_2_7.smv
LTL: false
CTL: false
INDEX: 8
FairPatrolling([r in l1, r in l2]),	NO,	DelayedReaction(cond,r exec act)

( ( AG (( AF (( state = l1))) & (AF (( state = l2)) ))) & (( AG (( ( state = l1)) -> (AX ( ! (E[ ( (  ! (( state = l1))) & ( ! (( state = l2)) )) U ((  ! ( ! (( state = l1)))) & ( ! (( state = l2)) ) ) ])) ))) & (AG (( ( state = l2)) -> (AX ( ! (E[ ( (  ! (( state = l2))) & ( ! (( state = l1)) )) U ((  ! ( ! (( state = l2)))) & ( ! (( state = l1)) ) ) ])) )) ) )) & (AG (( (cond)) -> (AF ((act)) )) )
( ( (  G ((  F ((l1))) & ( F ((l2)) ))) & ((  G (( (l1)) -> ( X (((  ! ((l1))) U ((l2) ) | ( G ( ! ((l1))) ) )) ))) & ( G (( (l2)) -> ( X (((  ! ((l2))) U ((l1) ) | ( G ( ! ((l2))) ) )) )) ) )) & (TRUE )) & ( G (( (cond)) -> ( F ((act)) )) )
NuSMV/LTLmodel_2_8.smv
NuSMV/CTLmodel_2_8.smv
LTL: false
CTL: false
INDEX: 9
SequencedPatrolling([r in l1, r in l2]),	UpperRestrictedAvoidance(r in l3,2),	NO,	
( AG (AF (( ( state = l1)) & (AF (( state = l2)) )))) & ( ! (AF (( ( state = l3)) & (AX (AF (( ( state = l3)) & (AX (AF (( ( state = l3)) & (AX (AF (( state = l3))) ))) ))) ))) )
( (  G ( F (( (l1)) & ( F ((l2)) )))) & ( ! ( F (( (l3)) & ( X ( F (( (l3)) & ( X ( F (( (l3)) & ( X ( F ((l3))) ))) ))) ))) )) & (TRUE )
NuSMV/LTLmodel_2_9.smv
NuSMV/CTLmodel_2_9.smv
LTL: false
CTL: false
------------------------------------------------------------
Building: 3
------------------------------------------------------------
	---;	l7,cond;	l2;	l4,cond;
	l6,cond;	l9;	l8;	---;
	l5;	l0;	---;	---;
	l1,cond;	---;	---;	l3;
INDEX: 0
OrderedPatrolling([r in l1, r in l2]),	UpperRestrictedAvoidance(r in l3,2),	Wait(cond,r in l4)

( ( ( ( AG (AF (( ( state = l1)) & (AF (( state = l2)) )))) & (( TRUE) & (A[ (  ! (( state = l2))) U (( state = l1) ) ] ) )) & (( AG (( ( state = l2)) -> (AX (A[ (  ! (( state = l2))) U (( state = l1) ) ]) ))) & (AG (( ( state = l2)) -> (AX (A[ (  ! (( state = l2))) U (( state = l1) ) ]) )) ) )) & ( ! (AF (( ( state = l3)) & (AX (AF (( ( state = l3)) & (AX (AF (( ( state = l3)) & (AX (AF (( state = l3))) ))) ))) ))) )) & (A[ ( (cond)) U (( state = l4) ) ] )
( ( ( (  G ( F (( (l1)) & ( F ((l2)) )))) & ((  ! ((l2))) U ((l1) ) )) & ((  G (( (l2)) -> ( X ((  ! ((l2))) U ((l1) )) ))) & ( G (( (l2)) -> ( X ((  ! ((l2))) U ((l1) )) )) ) )) & ( ! ( F (( (l3)) & ( X ( F (( (l3)) & ( X ( F (( (l3)) & ( X ( F ((l3))) ))) ))) ))) )) & (( (cond)) U ((l4) ) )
NuSMV/LTLmodel_3_0.smv
NuSMV/CTLmodel_3_0.smv
LTL: false
CTL: false
INDEX: 1
FairVisit([r in l1, r in l2]),	NO,	DelayedReaction(cond,r exec act)

( ( ( AF (( state = l1))) & (AF (( state = l2)) )) & (( AG (( ( state = l1)) -> (AX ( ! (E[ ( (  ! (( state = l1))) & ( ! (( state = l2)) )) U ((  ! ( ! (( state = l1)))) & ( ! (( state = l2)) ) ) ])) ))) & (AG (( ( state = l2)) -> (AX ( ! (E[ ( (  ! (( state = l2))) & ( ! (( state = l1)) )) U ((  ! ( ! (( state = l2)))) & ( ! (( state = l1)) ) ) ])) )) ) )) & (AG (( (cond)) -> (AF ((act)) )) )
( ( ( (  F ((l1))) & ( F ((l2)) )) & ((  G (( (l1)) -> ( X (((  ! ((l1))) U ((l2) ) | ( G ( ! ((l1))) ) )) ))) & ( G (( (l2)) -> ( X (((  ! ((l2))) U ((l1) ) | ( G ( ! ((l2))) ) )) )) ) )) & (TRUE )) & ( G (( (cond)) -> ( F ((act)) )) )
NuSMV/LTLmodel_3_1.smv
NuSMV/CTLmodel_3_1.smv
LTL: true
CTL: true
INDEX: 2
StrictOrderedVisit([r in l1, r in l2]),	GlobalAvoidance(r in l3),	InstantaneousReaction(cond,r exec act)

( ( ( ( AF (( ( state = l1)) & (AF (( state = l2)) ))) & (A[ (  ! (( state = l2))) U (( state = l1) ) ] )) & (A[ (  ! (( state = l1))) U (( ( state = l1)) & (AX (A[ (  ! (( state = l1))) U (( state = l2) ) ]) ) ) ] )) & (AG ( ! (( state = l3))) )) & (AG (( (cond)) -> ((act) )) )
( ( ( (  F (( (l1)) & ( F ((l2)) ))) & ((  ! ((l2))) U ((l1) ) )) & ((  ! ((l1))) U (( (l1)) & ( X ((  ! ((l1))) U ((l2) )) ) ) )) & ( G ( ! ((l3))) )) & ( G (( (cond)) -> ((act) )) )
NuSMV/LTLmodel_3_2.smv
NuSMV/CTLmodel_3_2.smv
LTL: true
CTL: true
INDEX: 3
SequencedVisit([r in l1, r in l2]),	FutureAvoidance(cond,r in l3),	NO,	
( AF (( ( state = l1)) & (AF (( state = l2)) ))) & (AG (( (cond)) -> (AG ( ! (( state = l3))) )) )
( (  F (( (l1)) & ( F ((l2)) ))) & ( G (( (cond)) -> ( G ( ! ((l3))) )) )) & (TRUE )
NuSMV/LTLmodel_3_3.smv
NuSMV/CTLmodel_3_3.smv
LTL: true
CTL: true
INDEX: 4
OrderedVisit([r in l1, r in l2]),	PastAvoidance(cond,r in l3),	InstantaneousReaction(cond,r exec act)

( ( ( AF (( ( state = l1)) & (AF (( state = l2)) ))) & (A[ (  ! (( state = l2))) U (( state = l1) ) ] )) & (A[ (  ! (( state = l3))) U ((cond) ) ] )) & (AG (( (cond)) -> ((act) )) )
( ( (  F (( (l1)) & ( F ((l2)) ))) & ((  ! ((l2))) U ((l1) ) )) & ((  ! ((l3))) U ((cond) ) )) & ( G (( (cond)) -> ((act) )) )
NuSMV/LTLmodel_3_4.smv
NuSMV/CTLmodel_3_4.smv
LTL: true
CTL: true
INDEX: 5
Visit([r in l1, r in l2]),	LowerRestrictedAvoidance(r in l3,2),	BindedReaction(cond,r exec act)

( ( ( AF (( state = l1))) & (AF (( state = l2)) )) & (AF (( ( state = l3)) & (AX (AF (( state = l3))) )) )) & (AG (( (cond)) <-> ((act) )) )
( ( (  F ((l1))) & ( F ((l2)) )) & ( F (( (l3)) & ( X ( F ((l3))) )) )) & ( G (( (cond)) <-> ((act) )) )
NuSMV/LTLmodel_3_5.smv
NuSMV/CTLmodel_3_5.smv
LTL: false
CTL: false
INDEX: 6
StrictOrderedPatrolling([r in l1, r in l2]),	FutureAvoidance(cond,r in l3),	Wait(cond,r in l4)

( ( ( ( ( AG (AF (( ( state = l1)) & (AF (( state = l2)) )))) & (( TRUE) & (A[ (  ! (( state = l2))) U (( state = l1) ) ] ) )) & (( AG (( ( state = l2)) -> (AX (A[ (  ! (( state = l2))) U (( state = l1) ) ]) ))) & (AG (( ( state = l2)) -> (AX (A[ (  ! (( state = l2))) U (( state = l1) ) ]) )) ) )) & (( AG (( ( state = l1)) -> (AX (A[ (  ! (( state = l1))) U (( state = l2) ) ]) ))) & (AG (( ( state = l2)) -> (AX (A[ (  ! (( state = l2))) U (( state = l1) ) ]) )) ) )) & (AG (( (cond)) -> (AG ( ! (( state = l3))) )) )) & (A[ ( (cond)) U (( state = l4) ) ] )
( ( ( ( (  G ( F (( (l1)) & ( F ((l2)) )))) & ((  ! ((l2))) U ((l1) ) )) & ((  G (( (l2)) -> ( X ((  ! ((l2))) U ((l1) )) ))) & ( G (( (l2)) -> ( X ((  ! ((l2))) U ((l1) )) )) ) )) & ((  G (( (l1)) -> ( X ((  ! ((l1))) U ((l2) )) ))) & ( G (( (l2)) -> ( X ((  ! ((l2))) U ((l1) )) )) ) )) & ( G (( (cond)) -> ( G ( ! ((l3))) )) )) & (( (cond)) U ((l4) ) )
NuSMV/LTLmodel_3_6.smv
NuSMV/CTLmodel_3_6.smv
LTL: false
CTL: false
INDEX: 7
Patrolling([r in l1, r in l2]),	LowerRestrictedAvoidance(r in l3,2),	InstantaneousReaction(cond,r exec act)

( ( AG (( ( TRUE) & (AF (( state = l1)) )) & (AF (( state = l2)) ))) & (AF (( ( state = l3)) & (AX (AF (( state = l3))) )) )) & (AG (( (cond)) -> ((act) )) )
( (  G ((  F ((l1))) & ( F ((l2)) ))) & ( F (( (l3)) & ( X ( F ((l3))) )) )) & ( G (( (cond)) -> ((act) )) )
NuSMV/LTLmodel_3_7.smv
NuSMV/CTLmodel_3_7.smv
LTL: false
CTL: false
INDEX: 8
FairPatrolling([r in l1, r in l2]),	NO,	DelayedReaction(cond,r exec act)

( ( AG (( AF (( state = l1))) & (AF (( state = l2)) ))) & (( AG (( ( state = l1)) -> (AX ( ! (E[ ( (  ! (( state = l1))) & ( ! (( state = l2)) )) U ((  ! ( ! (( state = l1)))) & ( ! (( state = l2)) ) ) ])) ))) & (AG (( ( state = l2)) -> (AX ( ! (E[ ( (  ! (( state = l2))) & ( ! (( state = l1)) )) U ((  ! ( ! (( state = l2)))) & ( ! (( state = l1)) ) ) ])) )) ) )) & (AG (( (cond)) -> (AF ((act)) )) )
( ( (  G ((  F ((l1))) & ( F ((l2)) ))) & ((  G (( (l1)) -> ( X (((  ! ((l1))) U ((l2) ) | ( G ( ! ((l1))) ) )) ))) & ( G (( (l2)) -> ( X (((  ! ((l2))) U ((l1) ) | ( G ( ! ((l2))) ) )) )) ) )) & (TRUE )) & ( G (( (cond)) -> ( F ((act)) )) )
NuSMV/LTLmodel_3_8.smv
NuSMV/CTLmodel_3_8.smv
LTL: true
CTL: true
INDEX: 9
SequencedPatrolling([r in l1, r in l2]),	UpperRestrictedAvoidance(r in l3,2),	NO,	
( AG (AF (( ( state = l1)) & (AF (( state = l2)) )))) & ( ! (AF (( ( state = l3)) & (AX (AF (( ( state = l3)) & (AX (AF (( ( state = l3)) & (AX (AF (( state = l3))) ))) ))) ))) )
( (  G ( F (( (l1)) & ( F ((l2)) )))) & ( ! ( F (( (l3)) & ( X ( F (( (l3)) & ( X ( F (( (l3)) & ( X ( F ((l3))) ))) ))) ))) )) & (TRUE )
NuSMV/LTLmodel_3_9.smv
NuSMV/CTLmodel_3_9.smv
LTL: true
CTL: true
------------------------------------------------------------
Building: 4
------------------------------------------------------------
	---;	---;	---;	l7,cond;
	l9;	l0;	l1,cond;	l4;
	---;	l6;	l8,cond;	l5,cond;
	---;	l2;	---;	l3;
INDEX: 0
OrderedPatrolling([r in l1, r in l2]),	UpperRestrictedAvoidance(r in l3,2),	Wait(cond,r in l4)

( ( ( ( AG (AF (( ( state = l1)) & (AF (( state = l2)) )))) & (( TRUE) & (A[ (  ! (( state = l2))) U (( state = l1) ) ] ) )) & (( AG (( ( state = l2)) -> (AX (A[ (  ! (( state = l2))) U (( state = l1) ) ]) ))) & (AG (( ( state = l2)) -> (AX (A[ (  ! (( state = l2))) U (( state = l1) ) ]) )) ) )) & ( ! (AF (( ( state = l3)) & (AX (AF (( ( state = l3)) & (AX (AF (( ( state = l3)) & (AX (AF (( state = l3))) ))) ))) ))) )) & (A[ ( (cond)) U (( state = l4) ) ] )
( ( ( (  G ( F (( (l1)) & ( F ((l2)) )))) & ((  ! ((l2))) U ((l1) ) )) & ((  G (( (l2)) -> ( X ((  ! ((l2))) U ((l1) )) ))) & ( G (( (l2)) -> ( X ((  ! ((l2))) U ((l1) )) )) ) )) & ( ! ( F (( (l3)) & ( X ( F (( (l3)) & ( X ( F (( (l3)) & ( X ( F ((l3))) ))) ))) ))) )) & (( (cond)) U ((l4) ) )
NuSMV/LTLmodel_4_0.smv
NuSMV/CTLmodel_4_0.smv
LTL: false
CTL: false
INDEX: 1
FairVisit([r in l1, r in l2]),	NO,	DelayedReaction(cond,r exec act)

( ( ( AF (( state = l1))) & (AF (( state = l2)) )) & (( AG (( ( state = l1)) -> (AX ( ! (E[ ( (  ! (( state = l1))) & ( ! (( state = l2)) )) U ((  ! ( ! (( state = l1)))) & ( ! (( state = l2)) ) ) ])) ))) & (AG (( ( state = l2)) -> (AX ( ! (E[ ( (  ! (( state = l2))) & ( ! (( state = l1)) )) U ((  ! ( ! (( state = l2)))) & ( ! (( state = l1)) ) ) ])) )) ) )) & (AG (( (cond)) -> (AF ((act)) )) )
( ( ( (  F ((l1))) & ( F ((l2)) )) & ((  G (( (l1)) -> ( X (((  ! ((l1))) U ((l2) ) | ( G ( ! ((l1))) ) )) ))) & ( G (( (l2)) -> ( X (((  ! ((l2))) U ((l1) ) | ( G ( ! ((l2))) ) )) )) ) )) & (TRUE )) & ( G (( (cond)) -> ( F ((act)) )) )
NuSMV/LTLmodel_4_1.smv
NuSMV/CTLmodel_4_1.smv
LTL: false
CTL: false
INDEX: 2
StrictOrderedVisit([r in l1, r in l2]),	GlobalAvoidance(r in l3),	InstantaneousReaction(cond,r exec act)

( ( ( ( AF (( ( state = l1)) & (AF (( state = l2)) ))) & (A[ (  ! (( state = l2))) U (( state = l1) ) ] )) & (A[ (  ! (( state = l1))) U (( ( state = l1)) & (AX (A[ (  ! (( state = l1))) U (( state = l2) ) ]) ) ) ] )) & (AG ( ! (( state = l3))) )) & (AG (( (cond)) -> ((act) )) )
( ( ( (  F (( (l1)) & ( F ((l2)) ))) & ((  ! ((l2))) U ((l1) ) )) & ((  ! ((l1))) U (( (l1)) & ( X ((  ! ((l1))) U ((l2) )) ) ) )) & ( G ( ! ((l3))) )) & ( G (( (cond)) -> ((act) )) )
NuSMV/LTLmodel_4_2.smv
NuSMV/CTLmodel_4_2.smv
LTL: false
CTL: false
INDEX: 3
SequencedVisit([r in l1, r in l2]),	FutureAvoidance(cond,r in l3),	NO,	
( AF (( ( state = l1)) & (AF (( state = l2)) ))) & (AG (( (cond)) -> (AG ( ! (( state = l3))) )) )
( (  F (( (l1)) & ( F ((l2)) ))) & ( G (( (cond)) -> ( G ( ! ((l3))) )) )) & (TRUE )
NuSMV/LTLmodel_4_3.smv
NuSMV/CTLmodel_4_3.smv
LTL: false
CTL: false
INDEX: 4
OrderedVisit([r in l1, r in l2]),	PastAvoidance(cond,r in l3),	InstantaneousReaction(cond,r exec act)

( ( ( AF (( ( state = l1)) & (AF (( state = l2)) ))) & (A[ (  ! (( state = l2))) U (( state = l1) ) ] )) & (A[ (  ! (( state = l3))) U ((cond) ) ] )) & (AG (( (cond)) -> ((act) )) )
( ( (  F (( (l1)) & ( F ((l2)) ))) & ((  ! ((l2))) U ((l1) ) )) & ((  ! ((l3))) U ((cond) ) )) & ( G (( (cond)) -> ((act) )) )
NuSMV/LTLmodel_4_4.smv
NuSMV/CTLmodel_4_4.smv
LTL: false
CTL: false
INDEX: 5
Visit([r in l1, r in l2]),	LowerRestrictedAvoidance(r in l3,2),	BindedReaction(cond,r exec act)

( ( ( AF (( state = l1))) & (AF (( state = l2)) )) & (AF (( ( state = l3)) & (AX (AF (( state = l3))) )) )) & (AG (( (cond)) <-> ((act) )) )
( ( (  F ((l1))) & ( F ((l2)) )) & ( F (( (l3)) & ( X ( F ((l3))) )) )) & ( G (( (cond)) <-> ((act) )) )
NuSMV/LTLmodel_4_5.smv
NuSMV/CTLmodel_4_5.smv
LTL: false
CTL: false
INDEX: 6
StrictOrderedPatrolling([r in l1, r in l2]),	FutureAvoidance(cond,r in l3),	Wait(cond,r in l4)

( ( ( ( ( AG (AF (( ( state = l1)) & (AF (( state = l2)) )))) & (( TRUE) & (A[ (  ! (( state = l2))) U (( state = l1) ) ] ) )) & (( AG (( ( state = l2)) -> (AX (A[ (  ! (( state = l2))) U (( state = l1) ) ]) ))) & (AG (( ( state = l2)) -> (AX (A[ (  ! (( state = l2))) U (( state = l1) ) ]) )) ) )) & (( AG (( ( state = l1)) -> (AX (A[ (  ! (( state = l1))) U (( state = l2) ) ]) ))) & (AG (( ( state = l2)) -> (AX (A[ (  ! (( state = l2))) U (( state = l1) ) ]) )) ) )) & (AG (( (cond)) -> (AG ( ! (( state = l3))) )) )) & (A[ ( (cond)) U (( state = l4) ) ] )
( ( ( ( (  G ( F (( (l1)) & ( F ((l2)) )))) & ((  ! ((l2))) U ((l1) ) )) & ((  G (( (l2)) -> ( X ((  ! ((l2))) U ((l1) )) ))) & ( G (( (l2)) -> ( X ((  ! ((l2))) U ((l1) )) )) ) )) & ((  G (( (l1)) -> ( X ((  ! ((l1))) U ((l2) )) ))) & ( G (( (l2)) -> ( X ((  ! ((l2))) U ((l1) )) )) ) )) & ( G (( (cond)) -> ( G ( ! ((l3))) )) )) & (( (cond)) U ((l4) ) )
NuSMV/LTLmodel_4_6.smv
NuSMV/CTLmodel_4_6.smv
LTL: false
CTL: false
INDEX: 7
Patrolling([r in l1, r in l2]),	LowerRestrictedAvoidance(r in l3,2),	InstantaneousReaction(cond,r exec act)

( ( AG (( ( TRUE) & (AF (( state = l1)) )) & (AF (( state = l2)) ))) & (AF (( ( state = l3)) & (AX (AF (( state = l3))) )) )) & (AG (( (cond)) -> ((act) )) )
( (  G ((  F ((l1))) & ( F ((l2)) ))) & ( F (( (l3)) & ( X ( F ((l3))) )) )) & ( G (( (cond)) -> ((act) )) )
NuSMV/LTLmodel_4_7.smv
NuSMV/CTLmodel_4_7.smv
LTL: false
CTL: false
INDEX: 8
FairPatrolling([r in l1, r in l2]),	NO,	DelayedReaction(cond,r exec act)

( ( AG (( AF (( state = l1))) & (AF (( state = l2)) ))) & (( AG (( ( state = l1)) -> (AX ( ! (E[ ( (  ! (( state = l1))) & ( ! (( state = l2)) )) U ((  ! ( ! (( state = l1)))) & ( ! (( state = l2)) ) ) ])) ))) & (AG (( ( state = l2)) -> (AX ( ! (E[ ( (  ! (( state = l2))) & ( ! (( state = l1)) )) U ((  ! ( ! (( state = l2)))) & ( ! (( state = l1)) ) ) ])) )) ) )) & (AG (( (cond)) -> (AF ((act)) )) )
( ( (  G ((  F ((l1))) & ( F ((l2)) ))) & ((  G (( (l1)) -> ( X (((  ! ((l1))) U ((l2) ) | ( G ( ! ((l1))) ) )) ))) & ( G (( (l2)) -> ( X (((  ! ((l2))) U ((l1) ) | ( G ( ! ((l2))) ) )) )) ) )) & (TRUE )) & ( G (( (cond)) -> ( F ((act)) )) )
NuSMV/LTLmodel_4_8.smv
NuSMV/CTLmodel_4_8.smv
LTL: false
CTL: false
INDEX: 9
SequencedPatrolling([r in l1, r in l2]),	UpperRestrictedAvoidance(r in l3,2),	NO,	
( AG (AF (( ( state = l1)) & (AF (( state = l2)) )))) & ( ! (AF (( ( state = l3)) & (AX (AF (( ( state = l3)) & (AX (AF (( ( state = l3)) & (AX (AF (( state = l3))) ))) ))) ))) )
( (  G ( F (( (l1)) & ( F ((l2)) )))) & ( ! ( F (( (l3)) & ( X ( F (( (l3)) & ( X ( F (( (l3)) & ( X ( F ((l3))) ))) ))) ))) )) & (TRUE )
NuSMV/LTLmodel_4_9.smv
NuSMV/CTLmodel_4_9.smv
LTL: false
CTL: false
------------------------------------------------------------
Building: 5
------------------------------------------------------------
	---;	---;	---;	l7;
	---;	l8;	l5,cond;	l1;
	---;	l4;	---;	l0;
	l2;	l3,cond;	l9,cond;	l6,cond;
INDEX: 0
OrderedPatrolling([r in l1, r in l2]),	UpperRestrictedAvoidance(r in l3,2),	Wait(cond,r in l4)

( ( ( ( AG (AF (( ( state = l1)) & (AF (( state = l2)) )))) & (( TRUE) & (A[ (  ! (( state = l2))) U (( state = l1) ) ] ) )) & (( AG (( ( state = l2)) -> (AX (A[ (  ! (( state = l2))) U (( state = l1) ) ]) ))) & (AG (( ( state = l2)) -> (AX (A[ (  ! (( state = l2))) U (( state = l1) ) ]) )) ) )) & ( ! (AF (( ( state = l3)) & (AX (AF (( ( state = l3)) & (AX (AF (( ( state = l3)) & (AX (AF (( state = l3))) ))) ))) ))) )) & (A[ ( (cond)) U (( state = l4) ) ] )
( ( ( (  G ( F (( (l1)) & ( F ((l2)) )))) & ((  ! ((l2))) U ((l1) ) )) & ((  G (( (l2)) -> ( X ((  ! ((l2))) U ((l1) )) ))) & ( G (( (l2)) -> ( X ((  ! ((l2))) U ((l1) )) )) ) )) & ( ! ( F (( (l3)) & ( X ( F (( (l3)) & ( X ( F (( (l3)) & ( X ( F ((l3))) ))) ))) ))) )) & (( (cond)) U ((l4) ) )
NuSMV/LTLmodel_5_0.smv
NuSMV/CTLmodel_5_0.smv
LTL: false
CTL: false
INDEX: 1
FairVisit([r in l1, r in l2]),	NO,	DelayedReaction(cond,r exec act)

( ( ( AF (( state = l1))) & (AF (( state = l2)) )) & (( AG (( ( state = l1)) -> (AX ( ! (E[ ( (  ! (( state = l1))) & ( ! (( state = l2)) )) U ((  ! ( ! (( state = l1)))) & ( ! (( state = l2)) ) ) ])) ))) & (AG (( ( state = l2)) -> (AX ( ! (E[ ( (  ! (( state = l2))) & ( ! (( state = l1)) )) U ((  ! ( ! (( state = l2)))) & ( ! (( state = l1)) ) ) ])) )) ) )) & (AG (( (cond)) -> (AF ((act)) )) )
( ( ( (  F ((l1))) & ( F ((l2)) )) & ((  G (( (l1)) -> ( X (((  ! ((l1))) U ((l2) ) | ( G ( ! ((l1))) ) )) ))) & ( G (( (l2)) -> ( X (((  ! ((l2))) U ((l1) ) | ( G ( ! ((l2))) ) )) )) ) )) & (TRUE )) & ( G (( (cond)) -> ( F ((act)) )) )
NuSMV/LTLmodel_5_1.smv
NuSMV/CTLmodel_5_1.smv
LTL: true
CTL: true
INDEX: 2
StrictOrderedVisit([r in l1, r in l2]),	GlobalAvoidance(r in l3),	InstantaneousReaction(cond,r exec act)

( ( ( ( AF (( ( state = l1)) & (AF (( state = l2)) ))) & (A[ (  ! (( state = l2))) U (( state = l1) ) ] )) & (A[ (  ! (( state = l1))) U (( ( state = l1)) & (AX (A[ (  ! (( state = l1))) U (( state = l2) ) ]) ) ) ] )) & (AG ( ! (( state = l3))) )) & (AG (( (cond)) -> ((act) )) )
( ( ( (  F (( (l1)) & ( F ((l2)) ))) & ((  ! ((l2))) U ((l1) ) )) & ((  ! ((l1))) U (( (l1)) & ( X ((  ! ((l1))) U ((l2) )) ) ) )) & ( G ( ! ((l3))) )) & ( G (( (cond)) -> ((act) )) )
NuSMV/LTLmodel_5_2.smv
NuSMV/CTLmodel_5_2.smv
LTL: false
CTL: false
INDEX: 3
SequencedVisit([r in l1, r in l2]),	FutureAvoidance(cond,r in l3),	NO,	
( AF (( ( state = l1)) & (AF (( state = l2)) ))) & (AG (( (cond)) -> (AG ( ! (( state = l3))) )) )
( (  F (( (l1)) & ( F ((l2)) ))) & ( G (( (cond)) -> ( G ( ! ((l3))) )) )) & (TRUE )
NuSMV/LTLmodel_5_3.smv
NuSMV/CTLmodel_5_3.smv
LTL: false
CTL: false
INDEX: 4
OrderedVisit([r in l1, r in l2]),	PastAvoidance(cond,r in l3),	InstantaneousReaction(cond,r exec act)

( ( ( AF (( ( state = l1)) & (AF (( state = l2)) ))) & (A[ (  ! (( state = l2))) U (( state = l1) ) ] )) & (A[ (  ! (( state = l3))) U ((cond) ) ] )) & (AG (( (cond)) -> ((act) )) )
( ( (  F (( (l1)) & ( F ((l2)) ))) & ((  ! ((l2))) U ((l1) ) )) & ((  ! ((l3))) U ((cond) ) )) & ( G (( (cond)) -> ((act) )) )
NuSMV/LTLmodel_5_4.smv
NuSMV/CTLmodel_5_4.smv
LTL: false
CTL: false
INDEX: 5
Visit([r in l1, r in l2]),	LowerRestrictedAvoidance(r in l3,2),	BindedReaction(cond,r exec act)

( ( ( AF (( state = l1))) & (AF (( state = l2)) )) & (AF (( ( state = l3)) & (AX (AF (( state = l3))) )) )) & (AG (( (cond)) <-> ((act) )) )
( ( (  F ((l1))) & ( F ((l2)) )) & ( F (( (l3)) & ( X ( F ((l3))) )) )) & ( G (( (cond)) <-> ((act) )) )
NuSMV/LTLmodel_5_5.smv
NuSMV/CTLmodel_5_5.smv
LTL: true
CTL: true
INDEX: 6
StrictOrderedPatrolling([r in l1, r in l2]),	FutureAvoidance(cond,r in l3),	Wait(cond,r in l4)

( ( ( ( ( AG (AF (( ( state = l1)) & (AF (( state = l2)) )))) & (( TRUE) & (A[ (  ! (( state = l2))) U (( state = l1) ) ] ) )) & (( AG (( ( state = l2)) -> (AX (A[ (  ! (( state = l2))) U (( state = l1) ) ]) ))) & (AG (( ( state = l2)) -> (AX (A[ (  ! (( state = l2))) U (( state = l1) ) ]) )) ) )) & (( AG (( ( state = l1)) -> (AX (A[ (  ! (( state = l1))) U (( state = l2) ) ]) ))) & (AG (( ( state = l2)) -> (AX (A[ (  ! (( state = l2))) U (( state = l1) ) ]) )) ) )) & (AG (( (cond)) -> (AG ( ! (( state = l3))) )) )) & (A[ ( (cond)) U (( state = l4) ) ] )
( ( ( ( (  G ( F (( (l1)) & ( F ((l2)) )))) & ((  ! ((l2))) U ((l1) ) )) & ((  G (( (l2)) -> ( X ((  ! ((l2))) U ((l1) )) ))) & ( G (( (l2)) -> ( X ((  ! ((l2))) U ((l1) )) )) ) )) & ((  G (( (l1)) -> ( X ((  ! ((l1))) U ((l2) )) ))) & ( G (( (l2)) -> ( X ((  ! ((l2))) U ((l1) )) )) ) )) & ( G (( (cond)) -> ( G ( ! ((l3))) )) )) & (( (cond)) U ((l4) ) )
NuSMV/LTLmodel_5_6.smv
NuSMV/CTLmodel_5_6.smv
LTL: false
CTL: false
INDEX: 7
Patrolling([r in l1, r in l2]),	LowerRestrictedAvoidance(r in l3,2),	InstantaneousReaction(cond,r exec act)

( ( AG (( ( TRUE) & (AF (( state = l1)) )) & (AF (( state = l2)) ))) & (AF (( ( state = l3)) & (AX (AF (( state = l3))) )) )) & (AG (( (cond)) -> ((act) )) )
( (  G ((  F ((l1))) & ( F ((l2)) ))) & ( F (( (l3)) & ( X ( F ((l3))) )) )) & ( G (( (cond)) -> ((act) )) )
NuSMV/LTLmodel_5_7.smv
NuSMV/CTLmodel_5_7.smv
LTL: true
CTL: true
INDEX: 8
FairPatrolling([r in l1, r in l2]),	NO,	DelayedReaction(cond,r exec act)

( ( AG (( AF (( state = l1))) & (AF (( state = l2)) ))) & (( AG (( ( state = l1)) -> (AX ( ! (E[ ( (  ! (( state = l1))) & ( ! (( state = l2)) )) U ((  ! ( ! (( state = l1)))) & ( ! (( state = l2)) ) ) ])) ))) & (AG (( ( state = l2)) -> (AX ( ! (E[ ( (  ! (( state = l2))) & ( ! (( state = l1)) )) U ((  ! ( ! (( state = l2)))) & ( ! (( state = l1)) ) ) ])) )) ) )) & (AG (( (cond)) -> (AF ((act)) )) )
( ( (  G ((  F ((l1))) & ( F ((l2)) ))) & ((  G (( (l1)) -> ( X (((  ! ((l1))) U ((l2) ) | ( G ( ! ((l1))) ) )) ))) & ( G (( (l2)) -> ( X (((  ! ((l2))) U ((l1) ) | ( G ( ! ((l2))) ) )) )) ) )) & (TRUE )) & ( G (( (cond)) -> ( F ((act)) )) )
NuSMV/LTLmodel_5_8.smv
NuSMV/CTLmodel_5_8.smv
LTL: true
CTL: true
INDEX: 9
SequencedPatrolling([r in l1, r in l2]),	UpperRestrictedAvoidance(r in l3,2),	NO,	
( AG (AF (( ( state = l1)) & (AF (( state = l2)) )))) & ( ! (AF (( ( state = l3)) & (AX (AF (( ( state = l3)) & (AX (AF (( ( state = l3)) & (AX (AF (( state = l3))) ))) ))) ))) )
( (  G ( F (( (l1)) & ( F ((l2)) )))) & ( ! ( F (( (l3)) & ( X ( F (( (l3)) & ( X ( F (( (l3)) & ( X ( F ((l3))) ))) ))) ))) )) & (TRUE )
NuSMV/LTLmodel_5_9.smv
NuSMV/CTLmodel_5_9.smv
LTL: false
CTL: false
