etienne@virtualBoks:~/git/efsmt_coverts$ sbt
[info] Loading project definition from /home/etienne/git/efsmt_coverts/project
[info] Set current project to EFSMT_COverTS (in build file:/home/etienne/git/efsmt_coverts/)
efsmt_coverts> run -ptaDir imitator_examples/Imitator/FMS2 -imFile imitator_examples/interactionModels/FMS2.im
[warn] Scala version was updated by one of library dependencies:
[warn]  * org.scala-lang:scala-library:(2.10.4, 2.10.0, 2.9.1) -> 2.10.6
[warn] To force scalaVersion, add the following:
[warn]  ivyScala := ivyScala.value map { _.copy(overrideScalaVersion = true) }
[warn] Run 'evicted' to see detailed eviction warnings

Multiple main classes detected, select one to run:

 [1] org.TCH2Z3
 [2] org.GenPhilos
 [3] org.HA2Z3
 [4] org.Thermostat2Z3
 [5] org.RunEFTests
 [6] org.TestAssemblyZ3
 [7] org.TestPPL
 [8] org.PTA2EF
 [9] org.GenUppaal
 [10] org.PTAG2EF
 [11] org.TestAssembly

Enter number: 10

[info] Running org.PTAG2EF -ptaDir imitator_examples/Imitator/FMS2 -imFile imitator_examples/interactionModels/FMS2.im
[info] Debug: java.library.path= /usr/java/packages/lib/amd64:/usr/lib/x86_64-linux-gnu/jni:/lib/x86_64-linux-gnu:/usr/lib/x86_64-linux-gnu:/usr/lib/jni:/lib:/usr/lib
[info] 1.1
[info] im = Set(Set(Mill_O_B3_M, Robot1_O_B3_M), Set(Conveyor_B1_in, Spec1_B1_in), Set(Mill_O_B3_R2, Robot2_O_B3_R2), Set(Robot4_B4_out_R4), Set(Painting_O_B6_P), Set(Assembly_product), Set(Painting_B6_in_P), Set(Assembly_B6_out_A), Set(Lathe_B4_out_L), Set(Mill_B3_out_M), Set(Painting_I_B6_P), Set(Assembly_O_B5_A, Robot2_O_B5_A), Set(Conveyor_I_B2_C2, Robot3_I_B2_C2), Set(Lathe_B4_in_L), Set(Painting_B6_out_P), Set(Robot4_B6_in_R4), Set(Mill_I_B3_R1, Robot1_I_B3_R1), Set(Conveyor_O_B2_R3, Robot3_O_B2_R3), Set(Robot1_B3_in_R1), Set(Robot1_B1_out, Spec1_B1_out), Set(Assembly_B5_out_A), Set(Robot3_B2_out), Set(Robot2_B3_out_R2), Set(Assembly_O_B6_A, Painting_O_B6_A, Robot4_O_B6_A), Set(Conveyor_B2_in), Set(Conveyor_O_B1_R1, Robot1_O_B1_R1), Set(Mill_I_B3_M, Robot2_I_B3_M), Set(Robot2_B5_in_R2), Set(Lathe_I_B4_L, Robot4_I_B4_L), Set(Lathe_O_B4_R4, Robot4_O_B4_R4), Set(Assembly_I_B5_R2, Robot2_I_B5_R2), Set(Lathe_I_B4_R3, Robot3_I_B4_R3), Set(Assembly_I_B6_R4, Painting_I_B6_R4, Robot4_I_B6_R4), Set(Robot3_B4_in_R3), Set(Robot3_O_B4_L), Set(Conveyor_I_B1_C1, Robot1_I_B1_C1), Set(Mill_B3_in_M))                                                                                
[info] clks: List(clk_I_B6_R4,  clk_B6_in_P,  clk_B6_out_P,  clk_O_B6_P,  clk_I_B6_P,  clk_O_B6_A)                                                                                                                                           
[info] ptag2ef for file /home/etienne/git/efsmt_coverts/imitator_examples/Imitator/FMS2/painting.imi ta = (PaitingDevice,P0,Set(P3, P2, P0, P1, P4),Set((P2,Painting_O_B6_P,true,Set(),Set((D,0)),Set(),P0), (P3,Painting_I_B6_P,true,Set(),Set((E,0)),Set(),P4), (P0,Painting_I_B6_R4,true,Set(),Set((A,0)),Set(),P1), (P1,Painting_B6_out_P,true,Set(),Set((C,0)),Set(),P2), (P0,Painting_B6_in_P,true,Set(),Set((B,0)),Set(),P1), (P4,Painting_O_B6_A,true,Set(),Set((F,0)),Set(),P0)),Map(D -> clk_O_B6_P, A -> clk_I_B6_R4, E -> clk_I_B6_P, B -> clk_B6_in_P, C -> clk_B6_out_P, F -> clk_O_B6_A),Map(P3 -> true, P2 -> true, P0 -> true, P1 -> true, P4 -> true),Map())                                                         
[info] ptaH: (PaitingDeviceh,P0,Set(P3, P2, P0, P1, P4),Set((P1,Painting_B6_out_P,true,Set(),Set((C,0), (L,0)),Set(),P2), (P2,Painting_O_B6_P,true,Set(),Set((D,0), (I,0)),Set(),P0), (P0,Painting_B6_in_P,true,Set(),Set((B,0), (H,0)),Set(),P1), (P0,Painting_I_B6_R4,true,Set(),Set((A,0), (J,0)),Set(),P1), (P4,Painting_O_B6_A,true,Set(),Set((F,0), (G,0)),Set(),P0), (P3,Painting_I_B6_P,true,Set(),Set((E,0), (K,0)),Set(),P4)),Map(H -> hPainting_B6_in_P, D -> clk_O_B6_P, G -> hPainting_O_B6_A, I -> hPainting_O_B6_P, A -> clk_I_B6_R4, E -> clk_I_B6_P, J -> hPainting_I_B6_R4, B -> clk_B6_in_P, C -> clk_B6_out_P, F -> clk_O_B6_A, K -> hPainting_I_B6_P, L -> hPainting_B6_out_P),Map(P3 -> true, P2 -> true, P0 -> true, P1 -> true, P4 -> true),Map(),Set())                                                                                                                                                                                                    
[info] locsI = Map(P3 -> 0, P2 -> 1, P0 -> 2, P1 -> 3, P4 -> 4)                                                                                                                                                                              
[info] iniL = P0                                                                                                                                                                                                                             
[info] clks: List(clk_I_B3_R1,  clk_B3_in_M,  clk_B3_out_M,  clk_O_B3_M,  clk_I_B3_M,  clk_O_B3_R2 )                                                                                                                                         
[info] ptag2ef for file /home/etienne/git/efsmt_coverts/imitator_examples/Imitator/FMS2/mill.imi ta = (Mill,M0,Set(M2, M4, M0, M1, M3),Set((M1,Mill_B3_out_M,true,Set(),Set((C,0)),Set(),M2), (M3,Mill_I_B3_M,true,Set(),Set((E,0)),Set(),M4), (M0,Mill_B3_in_M,true,Set(),Set((B,0)),Set(),M3), (M0,Mill_I_B3_R1,true,Set(),Set((A,0)),Set(),M1), (M4,Mill_O_B3_R2,true,Set(),Set((F,0)),Set(),M0), (M2,Mill_O_B3_M,true,Set(),Set((D,0)),Set(),M0)),Map(B -> clk_B3_in_M, A -> p_B3_out_M, F -> clk_O_B3_R2, A -> clk_I_B3_R1, D -> clk_O_B3_M, C -> clk_B3_out_M, E -> clk_I_B3_M),Map(M2 -> true, M4 -> true, M0 -> true, M1 -> true, M3 -> true),Map())                                                                           
[info] ptaH: (Millh,M0,Set(M2, M4, M0, M1, M3),Set((M2,Mill_O_B3_M,true,Set(),Set((D,0), (K,0)),Set(),M0), (M0,Mill_I_B3_R1,true,Set(),Set((A,0), (M,0)),Set(),M1), (M3,Mill_I_B3_M,true,Set(),Set((E,0), (L,0)),Set(),M4), (M1,Mill_B3_out_M,true,Set(),Set((C,0), (I,0)),Set(),M2), (M4,Mill_O_B3_R2,true,Set(),Set((F,0), (J,0)),Set(),M0), (M0,Mill_B3_in_M,true,Set(),Set((B,0), (H,0)),Set(),M3)),Map(B -> clk_B3_in_M, A -> p_B3_out_M, F -> clk_O_B3_R2, M -> hMill_I_B3_R1, L -> hMill_I_B3_M, A -> clk_I_B3_R1, H -> hMill_B3_in_M, J -> hMill_O_B3_R2, K -> hMill_O_B3_M, D -> clk_O_B3_M, C -> clk_B3_out_M, I -> hMill_B3_out_M, E -> clk_I_B3_M),Map(M2 -> true, M4 -> true, M0 -> true, M1 -> true, M3 -> true),Map(),Set(p_B3_out_M))
[info] locsI = Map(M2 -> 0, M4 -> 1, M0 -> 2, M1 -> 3, M3 -> 4)
[info] iniL = M0
[info] clks: List(clk_I_B2_C2,  clk_B2_out,  clk_O_B2_R3,  clk_B4_in_R3,  clk_I_B4_R3,  clk_O_B4_L)
[info] ptag2ef for file /home/etienne/git/efsmt_coverts/imitator_examples/Imitator/FMS2/robot3.imi ta = (Robot3,R3_0,Set(R3_3, R3_2, R3_1, R3_5, R3_4, R3_0),Set((R3_0,Robot3_I_B2_C2,true,Set(),Set((A,0)),Set(),R3_1), (R3_1,Robot3_B2_out,-A >= -1,Set(),Set((B,0)),Set(),R3_2), (R3_4,Robot3_I_B4_R3,true,Set(),Set((E,0)),Set(),R3_5), (R3_5,Robot3_O_B4_L,true,Set(),Set((F,0)),Set(),R3_0), (R3_3,Robot3_B4_in_R3,true,Set(),Set((D,0)),Set(),R3_4), (R3_2,Robot3_O_B2_R3,true,Set(),Set((C,0)),Set(),R3_3)),Map(E -> clk_I_B4_R3, A -> clk_I_B2_C2, C -> clk_O_B2_R3, F -> clk_O_B4_L, D -> clk_B4_in_R3, B -> clk_B2_out),Map(R3_3 -> true, R3_2 -> true, R3_1 -> true, R3_5 -> true, R3_4 -> true, R3_0 -> true),Map())
[info] ptaH: (Robot3h,R3_0,Set(R3_3, R3_2, R3_1, R3_5, R3_4, R3_0),Set((R3_3,Robot3_B4_in_R3,true,Set(),Set((D,0), (L,0)),Set(),R3_4), (R3_5,Robot3_O_B4_L,true,Set(),Set((F,0), (J,0)),Set(),R3_0), (R3_4,Robot3_I_B4_R3,true,Set(),Set((E,0), (H,0)),Set(),R3_5), (R3_1,Robot3_B2_out,-A >= -1,Set(),Set((B,0), (G,0)),Set(),R3_2), (R3_2,Robot3_O_B2_R3,true,Set(),Set((C,0), (I,0)),Set(),R3_3), (R3_0,Robot3_I_B2_C2,true,Set(),Set((A,0), (K,0)),Set(),R3_1)),Map(E -> clk_I_B4_R3, H -> hRobot3_I_B4_R3, L -> hRobot3_B4_in_R3, A -> clk_I_B2_C2, C -> clk_O_B2_R3, J -> hRobot3_O_B4_L, F -> clk_O_B4_L, I -> hRobot3_O_B2_R3, K -> hRobot3_I_B2_C2, D -> clk_B4_in_R3, B -> clk_B2_out, G -> hRobot3_B2_out),Map(R3_3 -> true, R3_2 -> true, R3_1 -> true, R3_5 -> true, R3_4 -> true, R3_0 -> true),Map(),Set())
[info] locsI = Map(R3_3 -> 0, R3_2 -> 1, R3_1 -> 2, R3_5 -> 3, R3_4 -> 4, R3_0 -> 5)
[info] iniL = R3_0
[info] clks: List(clk_I_B1_C1,  clk_B1_out,  clk_O_B1_R1,  clk_B3_in_R1,  clk_I_B3_R1,  clk_O_B3_M)
[info] ptag2ef for file /home/etienne/git/efsmt_coverts/imitator_examples/Imitator/FMS2/robot1.imi ta = (Robot1,R1_0,Set(R1_4, R1_1, R1_5, R1_2, R1_3, R1_0),Set((R1_5,Robot1_O_B3_M,true,Set(),Set((F,0)),Set(),R1_0), (R1_1,Robot1_B1_out,-A >= -1,Set(),Set((B,0)),Set(),R1_2), (R1_0,Robot1_I_B1_C1,true,Set(),Set((A,0)),Set(),R1_1), (R1_2,Robot1_O_B1_R1,true,Set(),Set((C,0)),Set(),R1_3), (R1_3,Robot1_B3_in_R1,true,Set(),Set((D,0)),Set(),R1_4), (R1_4,Robot1_I_B3_R1,true,Set(),Set((E,0)),Set(),R1_5)),Map(B -> clk_B1_out, F -> clk_O_B3_M, D -> clk_B3_in_R1, C -> clk_O_B1_R1, E -> clk_I_B3_R1, A -> clk_I_B1_C1),Map(R1_4 -> true, R1_1 -> true, R1_5 -> true, R1_2 -> true, R1_3 -> true, R1_0 -> true),Map())
[info] ptaH: (Robot1h,R1_0,Set(R1_4, R1_1, R1_5, R1_2, R1_3, R1_0),Set((R1_2,Robot1_O_B1_R1,true,Set(),Set((C,0), (H,0)),Set(),R1_3), (R1_1,Robot1_B1_out,-A >= -1,Set(),Set((B,0), (J,0)),Set(),R1_2), (R1_3,Robot1_B3_in_R1,true,Set(),Set((D,0), (L,0)),Set(),R1_4), (R1_5,Robot1_O_B3_M,true,Set(),Set((F,0), (K,0)),Set(),R1_0), (R1_4,Robot1_I_B3_R1,true,Set(),Set((E,0), (I,0)),Set(),R1_5), (R1_0,Robot1_I_B1_C1,true,Set(),Set((A,0), (G,0)),Set(),R1_1)),Map(I -> hRobot1_I_B3_R1, G -> hRobot1_I_B1_C1, B -> clk_B1_out, J -> hRobot1_B1_out, F -> clk_O_B3_M, D -> clk_B3_in_R1, H -> hRobot1_O_B1_R1, C -> clk_O_B1_R1, E -> clk_I_B3_R1, A -> clk_I_B1_C1, L -> hRobot1_B3_in_R1, K -> hRobot1_O_B3_M),Map(R1_4 -> true, R1_1 -> true, R1_5 -> true, R1_2 -> true, R1_3 -> true, R1_0 -> true),Map(),Set())
[info] locsI = Map(R1_4 -> 0, R1_1 -> 1, R1_5 -> 2, R1_2 -> 3, R1_3 -> 4, R1_0 -> 5)
[info] iniL = R1_0
[info] clks: List(clk_I_B3_M,  clk_B3_out_R2,  clk_O_B3_R2,  clk_B5_in_R2,  clk_I_B5_R2,  clk_O_B5_A )
[info] ptag2ef for file /home/etienne/git/efsmt_coverts/imitator_examples/Imitator/FMS2/robot2.imi ta = (Robot2,R2_0,Set(R2_2, R2_5, R2_1, R2_4, R2_0, R2_3),Set((R2_5,Robot2_O_B5_A,true,Set(),Set((F,0)),Set(),R2_0), (R2_4,Robot2_I_B5_R2,true,Set(),Set((E,0)),Set(),R2_5), (R2_3,Robot2_B5_in_R2,true,Set(),Set((D,0)),Set(),R2_4), (R2_2,Robot2_O_B3_R2,true,Set(),Set((C,0)),Set(),R2_3), (R2_0,Robot2_I_B3_M,true,Set(),Set((A,0)),Set(),R2_1), (R2_1,Robot2_B3_out_R2,true,Set(),Set((B,0)),Set(),R2_2)),Map(B -> clk_B3_out_R2, F -> clk_O_B5_A, D -> clk_B5_in_R2, C -> clk_O_B3_R2, E -> clk_I_B5_R2, A -> clk_I_B3_M),Map(R2_2 -> true, R2_5 -> true, R2_1 -> true, R2_4 -> true, R2_0 -> true, R2_3 -> true),Map())
[info] ptaH: (Robot2h,R2_0,Set(R2_2, R2_5, R2_1, R2_4, R2_0, R2_3),Set((R2_5,Robot2_O_B5_A,true,Set(),Set((F,0), (I,0)),Set(),R2_0), (R2_0,Robot2_I_B3_M,true,Set(),Set((A,0), (K,0)),Set(),R2_1), (R2_3,Robot2_B5_in_R2,true,Set(),Set((D,0), (G,0)),Set(),R2_4), (R2_1,Robot2_B3_out_R2,true,Set(),Set((B,0), (L,0)),Set(),R2_2), (R2_2,Robot2_O_B3_R2,true,Set(),Set((C,0), (J,0)),Set(),R2_3), (R2_4,Robot2_I_B5_R2,true,Set(),Set((E,0), (H,0)),Set(),R2_5)),Map(K -> hRobot2_I_B3_M, B -> clk_B3_out_R2, L -> hRobot2_B3_out_R2, F -> clk_O_B5_A, H -> hRobot2_I_B5_R2, D -> clk_B5_in_R2, G -> hRobot2_B5_in_R2, J -> hRobot2_O_B3_R2, C -> clk_O_B3_R2, E -> clk_I_B5_R2, A -> clk_I_B3_M, I -> hRobot2_O_B5_A),Map(R2_2 -> true, R2_5 -> true, R2_1 -> true, R2_4 -> true, R2_0 -> true, R2_3 -> true),Map(),Set())
[info] locsI = Map(R2_2 -> 0, R2_5 -> 1, R2_1 -> 2, R2_4 -> 3, R2_0 -> 4, R2_3 -> 5)
[info] iniL = R2_0
[info] clks: List(clk_I_B5_R2,  clk_B5_out_A,  clk_O_B5_A,  clk_I_B6_R4,  clk_B6_out_A,  clk_O_B6_A,  clk_product)
[info] ptag2ef for file /home/etienne/git/efsmt_coverts/imitator_examples/Imitator/FMS2/assembly.imi ta = (AssemblyStation,A0,Set(A4, A5, A2, A1, A6, A3, A0),Set((A3,Assembly_I_B6_R4,true,Set(),Set((D,0)),Set(),A4), (A5,Assembly_O_B6_A,true,Set(),Set((F,0)),Set(),A6), (A1,Assembly_B5_out_A,true,Set(),Set((B,0)),Set(),A2), (A0,Assembly_I_B5_R2,true,Set(),Set((A,0)),Set(),A1), (A6,Assembly_product,true,Set(),Set((G,0)),Set(),A0), (A2,Assembly_O_B5_A,true,Set(),Set((C,0)),Set(),A3), (A4,Assembly_B6_out_A,-D >= -1,Set(),Set((E,0)),Set(),A5)),Map(D -> clk_I_B6_R4, C -> clk_O_B5_A, G -> clk_product, E -> clk_B6_out_A, A -> clk_I_B5_R2, B -> clk_B5_out_A, F -> clk_O_B6_A),Map(A4 -> true, A5 -> true, A2 -> true, A1 -> true, A6 -> true, A3 -> true, A0 -> true),Map())
[info] ptaH: (AssemblyStationh,A0,Set(A4, A5, A2, A1, A6, A3, A0),Set((A6,Assembly_product,true,Set(),Set((G,0), (N,0)),Set(),A0), (A4,Assembly_B6_out_A,-D >= -1,Set(),Set((E,0), (M,0)),Set(),A5), (A5,Assembly_O_B6_A,true,Set(),Set((F,0), (K,0)),Set(),A6), (A1,Assembly_B5_out_A,true,Set(),Set((B,0), (H,0)),Set(),A2), (A3,Assembly_I_B6_R4,true,Set(),Set((D,0), (J,0)),Set(),A4), (A0,Assembly_I_B5_R2,true,Set(),Set((A,0), (I,0)),Set(),A1), (A2,Assembly_O_B5_A,true,Set(),Set((C,0), (L,0)),Set(),A3)),Map(D -> clk_I_B6_R4, C -> clk_O_B5_A, G -> clk_product, E -> clk_B6_out_A, N -> hAssembly_product, A -> clk_I_B5_R2, I -> hAssembly_I_B5_R2, M -> hAssembly_B6_out_A, K -> hAssembly_O_B6_A, J -> hAssembly_I_B6_R4, B -> clk_B5_out_A, H -> hAssembly_B5_out_A, L -> hAssembly_O_B5_A, F -> clk_O_B6_A),Map(A4 -> true, A5 -> true, A2 -> true, A1 -> true, A6 -> true, A3 -> true, A0 -> true),Map(),Set())
[info] locsI = Map(A4 -> 0, A5 -> 1, A2 -> 2, A1 -> 3, A6 -> 4, A3 -> 5, A0 -> 6)
[info] iniL = A0
[info] clks: List(clk_B2_in,  clk_I_B2_C2,  clk_B2_R3 )
[info] ptag2ef for file /home/etienne/git/efsmt_coverts/imitator_examples/Imitator/FMS2/conveyor2.imi ta = (Conveyor2,C2_C0,Set(C2_C0, C2_C1, C2_C2),Set((C2_C0,Conveyor_B2_in,true,Set(),Set((A,0)),Set(),C2_C1), (C2_C1,Conveyor_I_B2_C2,-A >= -1,Set(),Set((B,0)),Set(),C2_C2), (C2_C2,Conveyor_O_B2_R3,true,Set(),Set((C,0)),Set(),C2_C0)),Map(A -> clk_B2_in, B -> clk_I_B2_C2, C -> clk_B2_R3),Map(C2_C0 -> true, C2_C1 -> true, C2_C2 -> true),Map())
[info] ptaH: (Conveyor2h,C2_C0,Set(C2_C0, C2_C1, C2_C2),Set((C2_C0,Conveyor_B2_in,true,Set(),Set((A,0), (D,0)),Set(),C2_C1), (C2_C1,Conveyor_I_B2_C2,-A >= -1,Set(),Set((B,0), (E,0)),Set(),C2_C2), (C2_C2,Conveyor_O_B2_R3,true,Set(),Set((C,0), (F,0)),Set(),C2_C0)),Map(F -> hConveyor_O_B2_R3, A -> clk_B2_in, B -> clk_I_B2_C2, C -> clk_B2_R3, D -> hConveyor_B2_in, E -> hConveyor_I_B2_C2),Map(C2_C0 -> true, C2_C1 -> true, C2_C2 -> true),Map(),Set())
[info] locsI = Map(C2_C0 -> 0, C2_C1 -> 1, C2_C2 -> 2)
[info] iniL = C2_C0
[info] clks: List(clk_B1_in,  clk_I_B1_C1,  clk_B1_R1 )
[info] ptag2ef for file /home/etienne/git/efsmt_coverts/imitator_examples/Imitator/FMS2/conveyor1.imi ta = (Conveyor1,C0,Set(C0, C1, C2),Set((C0,Conveyor_B1_in,true,Set(),Set((A,0)),Set(),C1), (C1,Conveyor_I_B1_C1,true,Set(),Set((B,0)),Set(),C2), (C2,Conveyor_O_B1_R1,true,Set(),Set((C,0)),Set(),C0)),Map(A -> clk_B1_in, B -> clk_I_B1_C1, C -> clk_B1_R1, A -> p_I_B1_C1),Map(C0 -> true, C1 -> true, C2 -> true),Map())
[info] ptaH: (Conveyor1h,C0,Set(C0, C1, C2),Set((C0,Conveyor_B1_in,true,Set(),Set((A,0), (E,0)),Set(),C1), (C1,Conveyor_I_B1_C1,true,Set(),Set((B,0), (F,0)),Set(),C2), (C2,Conveyor_O_B1_R1,true,Set(),Set((C,0), (G,0)),Set(),C0)),Map(A -> p_I_B1_C1, B -> clk_I_B1_C1, C -> clk_B1_R1, E -> hConveyor_B1_in, A -> clk_B1_in, F -> hConveyor_I_B1_C1, G -> hConveyor_O_B1_R1),Map(C0 -> true, C1 -> true, C2 -> true),Map(),Set(p_I_B1_C1))
[info] locsI = Map(C0 -> 0, C1 -> 1, C2 -> 2)
[info] iniL = C0
[info] clks: List(clk_I_B4_L,  clk_B4_out_R4,  clk_O_B4_R4,  clk_B6_in_R4,  clk_I_B6_R4,  clk_O_B6_A )
[info] ptag2ef for file /home/etienne/git/efsmt_coverts/imitator_examples/Imitator/FMS2/robot4.imi ta = (Robot2,R4_0,Set(R4_0, R4_4, R4_1, R4_5, R4_2, R4_3),Set((R4_3,Robot4_B6_in_R4,true,Set(),Set((D,0)),Set(),R4_4), (R4_2,Robot4_O_B4_R4,true,Set(),Set((C,0)),Set(),R4_3), (R4_5,Robot4_O_B6_A,true,Set(),Set((F,0)),Set(),R4_0), (R4_0,Robot4_I_B4_L,true,Set(),Set((A,0)),Set(),R4_1), (R4_4,Robot4_I_B6_R4,-D >= -1,Set(),Set((E,0)),Set(),R4_5), (R4_1,Robot4_B4_out_R4,true,Set(),Set((B,0)),Set(),R4_2)),Map(C -> clk_O_B4_R4, B -> clk_B4_out_R4, D -> clk_B6_in_R4, F -> clk_O_B6_A, E -> clk_I_B6_R4, A -> clk_I_B4_L),Map(R4_0 -> true, R4_4 -> true, R4_1 -> true, R4_5 -> true, R4_2 -> true, R4_3 -> true),Map())
[info] ptaH: (Robot2h,R4_0,Set(R4_0, R4_4, R4_1, R4_5, R4_2, R4_3),Set((R4_4,Robot4_I_B6_R4,-D >= -1,Set(),Set((E,0), (I,0)),Set(),R4_5), (R4_5,Robot4_O_B6_A,true,Set(),Set((F,0), (G,0)),Set(),R4_0), (R4_2,Robot4_O_B4_R4,true,Set(),Set((C,0), (L,0)),Set(),R4_3), (R4_3,Robot4_B6_in_R4,true,Set(),Set((D,0), (J,0)),Set(),R4_4), (R4_1,Robot4_B4_out_R4,true,Set(),Set((B,0), (K,0)),Set(),R4_2), (R4_0,Robot4_I_B4_L,true,Set(),Set((A,0), (H,0)),Set(),R4_1)),Map(C -> clk_O_B4_R4, B -> clk_B4_out_R4, D -> clk_B6_in_R4, J -> hRobot4_B6_in_R4, K -> hRobot4_B4_out_R4, L -> hRobot4_O_B4_R4, F -> clk_O_B6_A, G -> hRobot4_O_B6_A, H -> hRobot4_I_B4_L, I -> hRobot4_I_B6_R4, E -> clk_I_B6_R4, A -> clk_I_B4_L),Map(R4_0 -> true, R4_4 -> true, R4_1 -> true, R4_5 -> true, R4_2 -> true, R4_3 -> true),Map(),Set())
[info] locsI = Map(R4_0 -> 0, R4_4 -> 1, R4_1 -> 2, R4_5 -> 3, R4_2 -> 4, R4_3 -> 5)
[info] iniL = R4_0
[info] clks: List(clk_B1_in,  clk_B1_out)
[info] ptag2ef for file /home/etienne/git/efsmt_coverts/imitator_examples/Imitator/FMS2/spec1.imi ta = (Spec1,S0,Set(S0, S1, ERROR),Set((S0,Spec1_B1_in,true,Set(),Set((A,0)),Set(),S1), (S1,Spec1_B1_out,A > 3,Set(),Set((B,0)),Set(),ERROR), (S1,Spec1_B1_out,-A >= -3,Set(),Set((B,0)),Set(),S0), (S0,Spec1_B1_out,true,Set(),Set((B,0)),Set(),ERROR), (ERROR,Spec1_B1_out,A > 3,Set(),Set((B,0)),Set(),ERROR)),Map(A -> clk_B1_in, B -> clk_B1_out),Map(S0 -> true, S1 -> true, ERROR -> true),Map())
[info] ptaH: (Spec1h,S0,Set(S0, S1, ERROR),Set((S0,Spec1_B1_out,true,Set(),Set((B,0), (D,0)),Set(),ERROR), (S1,Spec1_B1_out,A > 3,Set(),Set((B,0), (D,0)),Set(),ERROR), (S0,Spec1_B1_in,true,Set(),Set((A,0), (C,0)),Set(),S1), (ERROR,Spec1_B1_out,A > 3,Set(),Set((B,0), (D,0)),Set(),ERROR), (S1,Spec1_B1_out,-A >= -3,Set(),Set((B,0), (D,0)),Set(),S0)),Map(A -> clk_B1_in, B -> clk_B1_out, C -> hSpec1_B1_in, D -> hSpec1_B1_out),Map(S0 -> true, S1 -> true, ERROR -> true),Map(),Set())
[info] locsI = Map(S0 -> 0, S1 -> 1, ERROR -> 2)
[info] iniL = S0
[info] clks: List(clk_I_B4_R3,  clk_B4_in_L,  clk_B4_out_L,  clk_O_B4_L,  clk_I_B4_L,  clk_O_B4_R4 )
[info] ptag2ef for file /home/etienne/git/efsmt_coverts/imitator_examples/Imitator/FMS2/lathe.imi ta = (Lathe,Lathe0,Set(Lathe2, Lathe1, Lathe4, Lathe0, Lathe3),Set((Lathe3,Lathe_I_B4_L,true,Set(),Set((E,0)),Set(),Lathe4), (Lathe1,Lathe_B4_out_L,true,Set(),Set((C,0)),Set(),Lathe2), (Lathe4,Lathe_O_B4_R4,true,Set(),Set((F,0)),Set(),Lathe0), (Lathe2,Lathe_O_B4_L,true,Set(),Set((D,0)),Set(),Lathe0), (Lathe0,Lathe_B4_in_L,true,Set(),Set((B,0)),Set(),Lathe3), (Lathe0,Lathe_I_B4_R3,true,Set(),Set((A,0)),Set(),Lathe1)),Map(C -> clk_B4_out_L, B -> clk_B4_in_L, D -> clk_O_B4_L, F -> clk_O_B4_R4, E -> clk_I_B4_L, A -> clk_I_B4_R3),Map(Lathe2 -> true, Lathe1 -> true, Lathe4 -> true, Lathe0 -> true, Lathe3 -> true),Map())
[info] ptaH: (Latheh,Lathe0,Set(Lathe2, Lathe1, Lathe4, Lathe0, Lathe3),Set((Lathe0,Lathe_B4_in_L,true,Set(),Set((B,0), (L,0)),Set(),Lathe3), (Lathe4,Lathe_O_B4_R4,true,Set(),Set((F,0), (G,0)),Set(),Lathe0), (Lathe1,Lathe_B4_out_L,true,Set(),Set((C,0), (J,0)),Set(),Lathe2), (Lathe2,Lathe_O_B4_L,true,Set(),Set((D,0), (K,0)),Set(),Lathe0), (Lathe0,Lathe_I_B4_R3,true,Set(),Set((A,0), (I,0)),Set(),Lathe1), (Lathe3,Lathe_I_B4_L,true,Set(),Set((E,0), (H,0)),Set(),Lathe4)),Map(C -> clk_B4_out_L, B -> clk_B4_in_L, L -> hLathe_B4_in_L, D -> clk_O_B4_L, K -> hLathe_O_B4_L, J -> hLathe_B4_out_L, F -> clk_O_B4_R4, E -> clk_I_B4_L, G -> hLathe_O_B4_R4, A -> clk_I_B4_R3, H -> hLathe_I_B4_L, I -> hLathe_I_B4_R3),Map(Lathe2 -> true, Lathe1 -> true, Lathe4 -> true, Lathe0 -> true, Lathe3 -> true),Map(),Set())
[info] locsI = Map(Lathe2 -> 0, Lathe1 -> 1, Lathe4 -> 2, Lathe0 -> 3, Lathe3 -> 4)
[info] iniL = Lathe0