






































































































































































Loading Util.tlv $Revision: 4.3 $
Loading MCTL.tlv $Revision: 4.3 $
Loading MCTLS.tlv $Revision: 4.1 $
Loading TESTER.tlv $Revision: 4.2 $
Loading MCsimple.tlv  $Revision: 4.2 $
Loading SIMULATE $Revision: 4.2 $
Loading Floyd.tlv $Revision: 4.1 $
Loading Abstract.tlv  $Revision: 4.2 $
Loading deductive.tlv $Revision: 4.2 $
















 Check Realizability

 Specification is realizable 

 Check that a symbolic strategy is correct

Transition relation is complete

 All winning states satisfy invariant

 Automaton States

State 1
In.action = nil,    In.T1.loc = 0,      In.S1.loc = 0,      In.S2.loc = 0,
In.S3.loc = 0,      In.S4.loc = 0,      In.S5.loc = 0,      Out.index = 0,

State 2
In.action = voloA,  In.T1.loc = 0,      In.S1.loc = 0,      In.S2.loc = 0,
In.S3.loc = 0,      In.S4.loc = 0,      In.S5.loc = 0,      Out.index = 5,

State 3
In.action = searchHotelByZone,          In.T1.loc = 1,      In.S1.loc = 0,
In.S2.loc = 0,      In.S3.loc = 0,      In.S4.loc = 0,      In.S5.loc = 1,
Out.index = 4,

State 4
In.action = searchHotelByCategory,      In.T1.loc = 1,      In.S1.loc = 0,
In.S2.loc = 0,      In.S3.loc = 0,      In.S4.loc = 0,      In.S5.loc = 1,
Out.index = 3,

State 5
In.action = voloR,  In.T1.loc = 1,      In.S1.loc = 0,      In.S2.loc = 0,
In.S3.loc = 0,      In.S4.loc = 0,      In.S5.loc = 1,      Out.index = 5,

State 6
In.action = pagamento,                  In.T1.loc = 1,      In.S1.loc = 0,
In.S2.loc = 0,      In.S3.loc = 0,      In.S4.loc = 0,      In.S5.loc = 1,
Out.index = 5,

State 7
In.action = nil,    In.T1.loc = 3,      In.S1.loc = 0,      In.S2.loc = 0,
In.S3.loc = 0,      In.S4.loc = 0,      In.S5.loc = 3,      Out.index = 5,

State 8
In.action = searchHotelByZone,          In.T1.loc = 2,      In.S1.loc = 0,
In.S2.loc = 0,      In.S3.loc = 0,      In.S4.loc = 0,      In.S5.loc = 2,
Out.index = 4,

State 9
In.action = searchHotelByCategory,      In.T1.loc = 2,      In.S1.loc = 0,
In.S2.loc = 0,      In.S3.loc = 0,      In.S4.loc = 0,      In.S5.loc = 2,
Out.index = 3,

State 10
In.action = pagamento,                  In.T1.loc = 2,      In.S1.loc = 0,
In.S2.loc = 0,      In.S3.loc = 0,      In.S4.loc = 0,      In.S5.loc = 2,
Out.index = 5,

State 11
In.action = nil,    In.T1.loc = 4,      In.S1.loc = 0,      In.S2.loc = 0,
In.S3.loc = 0,      In.S4.loc = 0,      In.S5.loc = 3,      Out.index = 5,

State 12
In.action = searchCarByZone,            In.T1.loc = 6,      In.S1.loc = 0,
In.S2.loc = 0,      In.S3.loc = 1,      In.S4.loc = 0,      In.S5.loc = 2,
Out.index = 2,

State 13
In.action = searchCarByCategory,        In.T1.loc = 6,      In.S1.loc = 0,
In.S2.loc = 0,      In.S3.loc = 1,      In.S4.loc = 0,      In.S5.loc = 2,
Out.index = 1,

State 14
In.action = bookHotel,                  In.T1.loc = 6,      In.S1.loc = 0,
In.S2.loc = 0,      In.S3.loc = 1,      In.S4.loc = 0,      In.S5.loc = 2,
Out.index = 3,

State 15
In.action = bookCar,In.T1.loc = 8,      In.S1.loc = 1,      In.S2.loc = 0,
In.S3.loc = 1,      In.S4.loc = 0,      In.S5.loc = 2,      Out.index = 1,

State 16
In.action = bookCar,In.T1.loc = 8,      In.S1.loc = 0,      In.S2.loc = 1,
In.S3.loc = 1,      In.S4.loc = 0,      In.S5.loc = 2,      Out.index = 2,

State 17
In.action = searchCarByZone,            In.T1.loc = 6,      In.S1.loc = 0,
In.S2.loc = 0,      In.S3.loc = 0,      In.S4.loc = 1,      In.S5.loc = 2,
Out.index = 2,

State 18
In.action = searchCarByCategory,        In.T1.loc = 6,      In.S1.loc = 0,
In.S2.loc = 0,      In.S3.loc = 0,      In.S4.loc = 1,      In.S5.loc = 2,
Out.index = 1,

State 19
In.action = bookHotel,                  In.T1.loc = 6,      In.S1.loc = 0,
In.S2.loc = 0,      In.S3.loc = 0,      In.S4.loc = 1,      In.S5.loc = 2,
Out.index = 4,

State 20
In.action = bookCar,In.T1.loc = 8,      In.S1.loc = 1,      In.S2.loc = 0,
In.S3.loc = 0,      In.S4.loc = 1,      In.S5.loc = 2,      Out.index = 1,

State 21
In.action = bookCar,In.T1.loc = 8,      In.S1.loc = 0,      In.S2.loc = 1,
In.S3.loc = 0,      In.S4.loc = 1,      In.S5.loc = 2,      Out.index = 2,

State 22
In.action = searchCarByZone,            In.T1.loc = 5,      In.S1.loc = 0,
In.S2.loc = 0,      In.S3.loc = 1,      In.S4.loc = 0,      In.S5.loc = 1,
Out.index = 2,

State 23
In.action = searchCarByCategory,        In.T1.loc = 5,      In.S1.loc = 0,
In.S2.loc = 0,      In.S3.loc = 1,      In.S4.loc = 0,      In.S5.loc = 1,
Out.index = 1,

State 24
In.action = bookHotel,                  In.T1.loc = 5,      In.S1.loc = 0,
In.S2.loc = 0,      In.S3.loc = 1,      In.S4.loc = 0,      In.S5.loc = 1,
Out.index = 3,

State 25
In.action = bookCar,In.T1.loc = 7,      In.S1.loc = 1,      In.S2.loc = 0,
In.S3.loc = 1,      In.S4.loc = 0,      In.S5.loc = 1,      Out.index = 1,

State 26
In.action = bookCar,In.T1.loc = 7,      In.S1.loc = 0,      In.S2.loc = 1,
In.S3.loc = 1,      In.S4.loc = 0,      In.S5.loc = 1,      Out.index = 2,

State 27
In.action = searchCarByZone,            In.T1.loc = 5,      In.S1.loc = 0,
In.S2.loc = 0,      In.S3.loc = 0,      In.S4.loc = 1,      In.S5.loc = 1,
Out.index = 2,

State 28
In.action = searchCarByCategory,        In.T1.loc = 5,      In.S1.loc = 0,
In.S2.loc = 0,      In.S3.loc = 0,      In.S4.loc = 1,      In.S5.loc = 1,
Out.index = 1,

State 29
In.action = bookHotel,                  In.T1.loc = 5,      In.S1.loc = 0,
In.S2.loc = 0,      In.S3.loc = 0,      In.S4.loc = 1,      In.S5.loc = 1,
Out.index = 4,

State 30
In.action = bookCar,In.T1.loc = 7,      In.S1.loc = 1,      In.S2.loc = 0,
In.S3.loc = 0,      In.S4.loc = 1,      In.S5.loc = 1,      Out.index = 1,

State 31
In.action = bookCar,In.T1.loc = 7,      In.S1.loc = 0,      In.S2.loc = 1,
In.S3.loc = 0,      In.S4.loc = 1,      In.S5.loc = 1,      Out.index = 2,


 Automaton Transitions

From 1 to  2
From 2 to  3 4 5 6
From 3 to  27 28 29
From 4 to  22 23 24
From 5 to  8 9 10
From 6 to  7
From 7 to  7
From 8 to  17 18 19
From 9 to  12 13 14
From 10 to  11
From 11 to  11
From 12 to  16
From 13 to  15
From 14 to  8 9 10
From 15 to  12 13 14
From 16 to  12 13 14
From 17 to  21
From 18 to  20
From 19 to  8 9 10
From 20 to  17 18 19
From 21 to  17 18 19
From 22 to  26
From 23 to  25
From 24 to  3 4 5 6
From 25 to  22 23 24
From 26 to  22 23 24
From 27 to  31
From 28 to  30
From 29 to  3 4 5 6
From 30 to  27 28 29
From 31 to  27 28 29

Automaton has 31 states, and 70 transitions

