Class org.cte.ABCD.fiacre.tests.ABCDBaseExplorationTest

43

tests

0

failures

0

ignored

6.644s

duration

100%

successful

Tests

Test Duration Result
testN0 0.125s passed
testN10 1.249s passed
testN11 0.278s passed
testN12 0.248s passed
testN13 0.215s passed
testN14 0.266s passed
testN15 0.221s passed
testN16 0.188s passed
testN17 0.193s passed
testN18 0.183s passed
testN19 0.164s passed
testN2 0.105s passed
testN20 0.148s passed
testN21 0.043s passed
testN22 0.318s passed
testN23 0.148s passed
testN24 0.151s passed
testN25 0.150s passed
testN26 0.100s passed
testN27 0.093s passed
testN3 0.109s passed
testN30 0.023s passed
testN31 0.155s passed
testN32 0.116s passed
testN33 0.108s passed
testN34 0.096s passed
testN35 0.103s passed
testN36 0.036s passed
testN37 0.100s passed
testN38 0.094s passed
testN39 0.107s passed
testN4 0.109s passed
testN40 0.115s passed
testN41 0.029s passed
testN42 0.106s passed
testN43 0.118s passed
testN44 0.128s passed
testN5 0.031s passed
testN6 0.022s passed
testN7 0.088s passed
testN8 0.149s passed
testN9 0.085s passed
testPassing 0.031s passed

Standard output

[Converting ../ABCD/examples/example16_notused_mutex.abcd to fiacre]
------------------------------------------------------------------
[Compiling tmp/example16_notused_mutex.fcr]
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/resources/test
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/classes/main/abcd2fiacre
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/resources/main
[Exploring program test.compiled.example16_notused_mutex.Example16_notused_mutexRoot]
Exploring program 'test.compiled.example16_notused_mutex.Example16_notused_mutexRoot'.
--------------------Synthesis---------------------
Explored 1 states and 1 transitions in 0.003 seconds.
Exploration ended normally.
Result is stored in file '/Users/ciprian/Downloads/abcd-tests/abcd2fiacre/tmp/test.compiled.example16_notused_mutex.Example16_notused_mutexRoot.confs'.

--------------------Verification---------------------
--------------------Warning---------------------
Final states: 0

[Reading confs file tmp/test.compiled.example16_notused_mutex.Example16_notused_mutexRoot.confs]
Read configurations 1 and 1 actions.
[Converting ../ABCD/examples/example2-commSync.abcd to fiacre]
------------------------------------------------------------------
[Compiling tmp/example2_commSync.fcr]
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/resources/test
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/classes/main/abcd2fiacre
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/resources/main
[Exploring program test.compiled.example2_commsync.Example2_commSyncRoot]
Exploring program 'test.compiled.example2_commsync.Example2_commSyncRoot'.
--------------------Synthesis---------------------
Explored 2 states and 2 transitions in 0.002 seconds.
Exploration ended normally.
Result is stored in file '/Users/ciprian/Downloads/abcd-tests/abcd2fiacre/tmp/test.compiled.example2_commsync.Example2_commSyncRoot.confs'.

--------------------Verification---------------------
--------------------Warning---------------------
No warning.
[Reading confs file tmp/test.compiled.example2_commsync.Example2_commSyncRoot.confs]
Read configurations 2 and 2 actions.
[Converting ../ABCD/examples/example3-commASync.abcd to fiacre]
------------------------------------------------------------------
[Compiling tmp/example3_commASync.fcr]
Variable 'localV' in 'Fifo3block' is local to transitions.

Variable 'data' in 'ProcW' is constant.

incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/resources/test
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/classes/main/abcd2fiacre
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/resources/main
[Exploring program test.compiled.example3_commasync.Example3_commASyncRoot]
Exploring program 'test.compiled.example3_commasync.Example3_commASyncRoot'.
--------------------Synthesis---------------------
Explored 4 states and 8 transitions in 0.002 seconds.
Exploration ended normally.
Result is stored in file '/Users/ciprian/Downloads/abcd-tests/abcd2fiacre/tmp/test.compiled.example3_commasync.Example3_commASyncRoot.confs'.

--------------------Verification---------------------
--------------------Warning---------------------
No warning.
[Reading confs file tmp/test.compiled.example3_commasync.Example3_commASyncRoot.confs]
Read configurations 4 and 8 actions.
[Converting ../ABCD/examples/example3_async_2chan_b.abcd to fiacre]
------------------------------------------------------------------
[Compiling tmp/example3_async_2chan_b.fcr]
Variable 'localV' in 'Fifo2block' is local to transitions.

incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/resources/test
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/classes/main/abcd2fiacre
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/resources/main
[Exploring program test.compiled.example3_async_2chan_b.Example3_async_2chan_bRoot]
Exploring program 'test.compiled.example3_async_2chan_b.Example3_async_2chan_bRoot'.
--------------------Synthesis---------------------
Explored 36 states and 144 transitions in 0.008 seconds.
Exploration ended normally.
Result is stored in file '/Users/ciprian/Downloads/abcd-tests/abcd2fiacre/tmp/test.compiled.example3_async_2chan_b.Example3_async_2chan_bRoot.confs'.

--------------------Verification---------------------
--------------------Warning---------------------
No warning.
[Reading confs file tmp/test.compiled.example3_async_2chan_b.Example3_async_2chan_bRoot.confs]
Read configurations 36 and 144 actions.
[Converting ../ABCD/examples/example3_async_2chan_bnb.abcd to fiacre]
------------------------------------------------------------------
[Compiling tmp/example3_async_2chan_bnb.fcr]
Variable 'localV' in 'Fifo2block' is local to transitions.

Variable 'localV' in 'Fifo3noblock' is local to transitions.

Variable 'localV0' in 'ProcR0' is local to transitions.

incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/resources/test
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/classes/main/abcd2fiacre
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/resources/main
[Exploring program test.compiled.example3_async_2chan_bnb.Example3_async_2chan_bnbRoot]
Exploring program 'test.compiled.example3_async_2chan_bnb.Example3_async_2chan_bnbRoot'.
--------------------Synthesis---------------------
Explored 48 states and 192 transitions in 0.011 seconds.
Exploration ended normally.
Result is stored in file '/Users/ciprian/Downloads/abcd-tests/abcd2fiacre/tmp/test.compiled.example3_async_2chan_bnb.Example3_async_2chan_bnbRoot.confs'.

--------------------Verification---------------------
--------------------Warning---------------------
No warning.
[Reading confs file tmp/test.compiled.example3_async_2chan_bnb.Example3_async_2chan_bnbRoot.confs]
Read configurations 48 and 192 actions.
[Converting ../ABCD/examples/example3_async_2chan_nb.abcd to fiacre]
------------------------------------------------------------------
[Compiling tmp/example3_async_2chan_nb.fcr]
Variable 'localV' in 'Fifo2noblock' is local to transitions.

Variable 'localV1' in 'ProcR1' is local to transitions.

Variable 'localV0' in 'ProcR0' is local to transitions.

incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/resources/test
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/classes/main/abcd2fiacre
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/resources/main
[Exploring program test.compiled.example3_async_2chan_nb.Example3_async_2chan_nbRoot]
Exploring program 'test.compiled.example3_async_2chan_nb.Example3_async_2chan_nbRoot'.
--------------------Synthesis---------------------
Explored 36 states and 144 transitions in 0.008 seconds.
Exploration ended normally.
Result is stored in file '/Users/ciprian/Downloads/abcd-tests/abcd2fiacre/tmp/test.compiled.example3_async_2chan_nb.Example3_async_2chan_nbRoot.confs'.

--------------------Verification---------------------
--------------------Warning---------------------
No warning.
[Reading confs file tmp/test.compiled.example3_async_2chan_nb.Example3_async_2chan_nbRoot.confs]
Read configurations 36 and 144 actions.
[Converting ../ABCD/examples/example3_async_block.abcd to fiacre]
------------------------------------------------------------------
[Compiling tmp/example3_async_block.fcr]
Variable 'localV' in 'Fifo2block' is local to transitions.

incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/resources/test
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/classes/main/abcd2fiacre
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/resources/main
[Exploring program test.compiled.example3_async_block.Example3_async_blockRoot]
Exploring program 'test.compiled.example3_async_block.Example3_async_blockRoot'.
--------------------Synthesis---------------------
Explored 6 states and 12 transitions in 0.001 seconds.
Exploration ended normally.
Result is stored in file '/Users/ciprian/Downloads/abcd-tests/abcd2fiacre/tmp/test.compiled.example3_async_block.Example3_async_blockRoot.confs'.

--------------------Verification---------------------
--------------------Warning---------------------
No warning.
[Reading confs file tmp/test.compiled.example3_async_block.Example3_async_blockRoot.confs]
Read configurations 6 and 12 actions.
[Converting ../ABCD/examples/example3_async_noblock.abcd to fiacre]
------------------------------------------------------------------
[Compiling tmp/example3_async_noblock.fcr]
Variable 'localV' in 'Fifo2noblock' is local to transitions.

Variable 'localV0' in 'ProcR0' is local to transitions.

incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/resources/test
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/classes/main/abcd2fiacre
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/resources/main
[Exploring program test.compiled.example3_async_noblock.Example3_async_noblockRoot]
Exploring program 'test.compiled.example3_async_noblock.Example3_async_noblockRoot'.
--------------------Synthesis---------------------
Explored 6 states and 12 transitions in 0.002 seconds.
Exploration ended normally.
Result is stored in file '/Users/ciprian/Downloads/abcd-tests/abcd2fiacre/tmp/test.compiled.example3_async_noblock.Example3_async_noblockRoot.confs'.

--------------------Verification---------------------
--------------------Warning---------------------
No warning.
[Reading confs file tmp/test.compiled.example3_async_noblock.Example3_async_noblockRoot.confs]
Read configurations 6 and 12 actions.
[Converting ../ABCD/examples/example3_async_sync.abcd to fiacre]
------------------------------------------------------------------
[Compiling tmp/example3_async_sync.fcr]
Variable 'localV' in 'Fifo4block' is local to transitions.

incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/resources/test
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/classes/main/abcd2fiacre
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/resources/main
[Exploring program test.compiled.example3_async_sync.Example3_async_syncRoot]
Exploring program 'test.compiled.example3_async_sync.Example3_async_syncRoot'.
--------------------Synthesis---------------------
Explored 20 states and 60 transitions in 0.005 seconds.
Exploration ended normally.
Result is stored in file '/Users/ciprian/Downloads/abcd-tests/abcd2fiacre/tmp/test.compiled.example3_async_sync.Example3_async_syncRoot.confs'.

--------------------Verification---------------------
--------------------Warning---------------------
No warning.
[Reading confs file tmp/test.compiled.example3_async_sync.Example3_async_syncRoot.confs]
Read configurations 20 and 60 actions.
[Converting ../ABCD/examples/example3_async_sync_noblock.abcd to fiacre]
------------------------------------------------------------------
[Compiling tmp/example3_async_sync_noblock.fcr]
Variable 'localV' in 'Fifo4noblock' is local to transitions.

Variable 'localV0' in 'ProcR0' is local to transitions.

incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/resources/test
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/classes/main/abcd2fiacre
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/resources/main
[Exploring program test.compiled.example3_async_sync_noblock.Example3_async_sync_noblockRoot]
Exploring program 'test.compiled.example3_async_sync_noblock.Example3_async_sync_noblockRoot'.
--------------------Synthesis---------------------
Explored 20 states and 60 transitions in 0.003 seconds.
Exploration ended normally.
Result is stored in file '/Users/ciprian/Downloads/abcd-tests/abcd2fiacre/tmp/test.compiled.example3_async_sync_noblock.Example3_async_sync_noblockRoot.confs'.

--------------------Verification---------------------
--------------------Warning---------------------
No warning.
[Reading confs file tmp/test.compiled.example3_async_sync_noblock.Example3_async_sync_noblockRoot.confs]
Read configurations 20 and 60 actions.
[Converting ../ABCD/examples/example4-comput.abcd to fiacre]
------------------------------------------------------------------
[Compiling tmp/example4_comput.fcr]
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/resources/test
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/classes/main/abcd2fiacre
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/resources/main
[Exploring program test.compiled.example4_comput.Example4_computRoot]
Exploring program 'test.compiled.example4_comput.Example4_computRoot'.
--------------------Synthesis---------------------
Explored 11 states and 16 transitions in 0.003 seconds.
Exploration ended normally.
Result is stored in file '/Users/ciprian/Downloads/abcd-tests/abcd2fiacre/tmp/test.compiled.example4_comput.Example4_computRoot.confs'.

--------------------Verification---------------------
--------------------Warning---------------------
Final states: 9, 10

[Reading confs file tmp/test.compiled.example4_comput.Example4_computRoot.confs]
Read configurations 11 and 16 actions.
[Converting ../ABCD/examples/example5-prodCons.abcd to fiacre]
------------------------------------------------------------------
[Compiling tmp/example5_prodCons.fcr]
[Converting ../ABCD/examples/example5_prodCons_nomulti.abcd to fiacre]
------------------------------------------------------------------
[Compiling tmp/example5_prodCons_nomulti.fcr]
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/resources/test
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/classes/main/abcd2fiacre
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/resources/main
[Exploring program test.compiled.example5_prodcons_nomulti.Example5_prodCons_nomultiRoot]
Exploring program 'test.compiled.example5_prodcons_nomulti.Example5_prodCons_nomultiRoot'.
--------------------Synthesis---------------------
Explored 1,918 states and 3,836 transitions in 0.102 seconds.
Exploration ended normally.
Result is stored in file '/Users/ciprian/Downloads/abcd-tests/abcd2fiacre/tmp/test.compiled.example5_prodcons_nomulti.Example5_prodCons_nomultiRoot.confs'.

--------------------Verification---------------------
--------------------Warning---------------------
Final states: 1917

[Reading confs file tmp/test.compiled.example5_prodcons_nomulti.Example5_prodCons_nomultiRoot.confs]
Read configurations 1918 and 3836 actions.
[Converting ../ABCD/examples/example6-stack.abcd to fiacre]
------------------------------------------------------------------
[Compiling tmp/example6_stack.fcr]
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/resources/test
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/classes/main/abcd2fiacre
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/resources/main
[Exploring program test.compiled.example6_stack.Example6_stackRoot]
Exploring program 'test.compiled.example6_stack.Example6_stackRoot'.
--------------------Synthesis---------------------
Explored 99 states and 119 transitions in 0.002 seconds.
Exploration ended normally.
Result is stored in file '/Users/ciprian/Downloads/abcd-tests/abcd2fiacre/tmp/test.compiled.example6_stack.Example6_stackRoot.confs'.

--------------------Verification---------------------
--------------------Warning---------------------
No warning.
[Reading confs file tmp/test.compiled.example6_stack.Example6_stackRoot.confs]
Read configurations 99 and 119 actions.
[Converting ../ABCD/examples/example7-mutex.abcd to fiacre]
------------------------------------------------------------------
[Compiling tmp/example7_mutex.fcr]
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/resources/test
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/classes/main/abcd2fiacre
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/resources/main
[Exploring program test.compiled.example7_mutex.Example7_mutexRoot]
Exploring program 'test.compiled.example7_mutex.Example7_mutexRoot'.
--------------------Synthesis---------------------
Explored 39 states and 108 transitions in 0.003 seconds.
Exploration ended normally.
Result is stored in file '/Users/ciprian/Downloads/abcd-tests/abcd2fiacre/tmp/test.compiled.example7_mutex.Example7_mutexRoot.confs'.

--------------------Verification---------------------
--------------------Warning---------------------
No warning.
[Reading confs file tmp/test.compiled.example7_mutex.Example7_mutexRoot.confs]
Read configurations 39 and 108 actions.
[Converting ../ABCD/examples/example7-semaphore.abcd to fiacre]
------------------------------------------------------------------
[Compiling tmp/example7_semaphore.fcr]
Variable 'delta' in 'sem_2_2' is local to transitions.

incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/resources/test
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/classes/main/abcd2fiacre
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/resources/main
[Exploring program test.compiled.example7_semaphore.Example7_semaphoreRoot]
Exploring program 'test.compiled.example7_semaphore.Example7_semaphoreRoot'.
--------------------Synthesis---------------------
Explored 51 states and 204 transitions in 0.004 seconds.
Exploration ended normally.
Result is stored in file '/Users/ciprian/Downloads/abcd-tests/abcd2fiacre/tmp/test.compiled.example7_semaphore.Example7_semaphoreRoot.confs'.

--------------------Verification---------------------
--------------------Warning---------------------
Final states: 50

[Reading confs file tmp/test.compiled.example7_semaphore.Example7_semaphoreRoot.confs]
Read configurations 51 and 204 actions.
[Converting ../ABCD/examples/example7_local_semaphore.abcd to fiacre]
WARNING: local semaphore 'y' in process x will be removed
------------------------------------------------------------------
[Compiling tmp/example7_local_semaphore.fcr]
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/resources/test
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/classes/main/abcd2fiacre
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/resources/main
[Exploring program test.compiled.example7_local_semaphore.Example7_local_semaphoreRoot]
Exploring program 'test.compiled.example7_local_semaphore.Example7_local_semaphoreRoot'.
--------------------Synthesis---------------------
Explored 1 states and 1 transitions in 0.001 seconds.
Exploration ended normally.
Result is stored in file '/Users/ciprian/Downloads/abcd-tests/abcd2fiacre/tmp/test.compiled.example7_local_semaphore.Example7_local_semaphoreRoot.confs'.

--------------------Verification---------------------
--------------------Warning---------------------
Final states: 0

[Reading confs file tmp/test.compiled.example7_local_semaphore.Example7_local_semaphoreRoot.confs]
Read configurations 1 and 1 actions.
[Converting ../ABCD/examples/example7_notused_semaphore.abcd to fiacre]
------------------------------------------------------------------
[Compiling tmp/example7_notused_semaphore.fcr]
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/resources/test
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/classes/main/abcd2fiacre
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/resources/main
[Exploring program test.compiled.example7_notused_semaphore.Example7_notused_semaphoreRoot]
Exploring program 'test.compiled.example7_notused_semaphore.Example7_notused_semaphoreRoot'.
--------------------Synthesis---------------------
Explored 1 states and 1 transitions in 0 seconds.
Exploration ended normally.
Result is stored in file '/Users/ciprian/Downloads/abcd-tests/abcd2fiacre/tmp/test.compiled.example7_notused_semaphore.Example7_notused_semaphoreRoot.confs'.

--------------------Verification---------------------
--------------------Warning---------------------
Final states: 0

[Reading confs file tmp/test.compiled.example7_notused_semaphore.Example7_notused_semaphoreRoot.confs]
Read configurations 1 and 1 actions.
[Converting ../ABCD/examples/example_async_chan.abcd to fiacre]
------------------------------------------------------------------
[Compiling tmp/example_async_chan.fcr]
[Converting ../ABCD/examples/example_defer_lowlevel.abcd to fiacre]
------------------------------------------------------------------
[Compiling tmp/example_defer_lowlevel.fcr]
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/resources/test
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/classes/main/abcd2fiacre
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/resources/main
[Exploring program test.compiled.example_defer_lowlevel.Example_defer_lowlevelRoot]
Exploring program 'test.compiled.example_defer_lowlevel.Example_defer_lowlevelRoot'.
--------------------Synthesis---------------------
Explored 45 states and 111 transitions in 0.004 seconds.
Exploration ended normally.
Result is stored in file '/Users/ciprian/Downloads/abcd-tests/abcd2fiacre/tmp/test.compiled.example_defer_lowlevel.Example_defer_lowlevelRoot.confs'.

--------------------Verification---------------------
--------------------Warning---------------------
Final states: 37

[Reading confs file tmp/test.compiled.example_defer_lowlevel.Example_defer_lowlevelRoot.confs]
Read configurations 45 and 111 actions.
[Converting ../ABCD/examples/example_endloop.abcd to fiacre]
------------------------------------------------------------------
[Compiling tmp/example_endloop.fcr]
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/resources/test
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/classes/main/abcd2fiacre
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/resources/main
[Exploring program test.compiled.example_endloop.Example_endloopRoot]
Exploring program 'test.compiled.example_endloop.Example_endloopRoot'.
--------------------Synthesis---------------------
Explored 3 states and 3 transitions in 0.001 seconds.
Exploration ended normally.
Result is stored in file '/Users/ciprian/Downloads/abcd-tests/abcd2fiacre/tmp/test.compiled.example_endloop.Example_endloopRoot.confs'.

--------------------Verification---------------------
--------------------Warning---------------------
No warning.
[Reading confs file tmp/test.compiled.example_endloop.Example_endloopRoot.confs]
Read configurations 3 and 3 actions.
[Converting ../ABCD/examples/example_fct1.abcd to fiacre]
------------------------------------------------------------------
[Compiling tmp/example_fct1.fcr]
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/resources/test
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/classes/main/abcd2fiacre
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/resources/main
[Exploring program test.compiled.example_fct1.Example_fct1Root]
Exploring program 'test.compiled.example_fct1.Example_fct1Root'.
--------------------Synthesis---------------------
Explored 2 states and 2 transitions in 0.001 seconds.
Exploration ended normally.
Result is stored in file '/Users/ciprian/Downloads/abcd-tests/abcd2fiacre/tmp/test.compiled.example_fct1.Example_fct1Root.confs'.

--------------------Verification---------------------
--------------------Warning---------------------
Final states: 1

[Reading confs file tmp/test.compiled.example_fct1.Example_fct1Root.confs]
Read configurations 2 and 2 actions.
[Converting ../ABCD/examples/example_fifo_ops.abcd to fiacre]
------------------------------------------------------------------
[Compiling tmp/example_fifo_ops.fcr]
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/resources/test
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/classes/main/abcd2fiacre
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/resources/main
[Exploring program test.compiled.example_fifo_ops.Example_fifo_opsRoot]
Exploring program 'test.compiled.example_fifo_ops.Example_fifo_opsRoot'.
--------------------Synthesis---------------------
Explored 7 states and 7 transitions in 0.001 seconds.
Exploration ended normally.
Result is stored in file '/Users/ciprian/Downloads/abcd-tests/abcd2fiacre/tmp/test.compiled.example_fifo_ops.Example_fifo_opsRoot.confs'.

--------------------Verification---------------------
--------------------Warning---------------------
No warning.
[Reading confs file tmp/test.compiled.example_fifo_ops.Example_fifo_opsRoot.confs]
Read configurations 7 and 7 actions.
[Converting ../ABCD/examples/example_foreach.abcd to fiacre]
------------------------------------------------------------------
[Compiling tmp/example_foreach.fcr]
Variable 'i' in 'toto' is constant.

incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/resources/test
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/classes/main/abcd2fiacre
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/resources/main
[Exploring program test.compiled.example_foreach.Example_foreachRoot]
Exploring program 'test.compiled.example_foreach.Example_foreachRoot'.
--------------------Synthesis---------------------
Explored 2 states and 2 transitions in 0 seconds.
Exploration ended normally.
Result is stored in file '/Users/ciprian/Downloads/abcd-tests/abcd2fiacre/tmp/test.compiled.example_foreach.Example_foreachRoot.confs'.

--------------------Verification---------------------
--------------------Warning---------------------
Final states: 1

[Reading confs file tmp/test.compiled.example_foreach.Example_foreachRoot.confs]
Read configurations 2 and 2 actions.
[Converting ../ABCD/examples/example_ping_pong.abcd to fiacre]
------------------------------------------------------------------
[Compiling tmp/example_ping_pong.fcr]
[Converting ../ABCD/examples/example_portmap.abcd to fiacre]
------------------------------------------------------------------
[Compiling tmp/example_portmap.fcr]
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/resources/test
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/classes/main/abcd2fiacre
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/resources/main
[Exploring program test.compiled.example_portmap.Example_portmapRoot]
Exploring program 'test.compiled.example_portmap.Example_portmapRoot'.
--------------------Synthesis---------------------
Explored 4 states and 6 transitions in 0.001 seconds.
Exploration ended normally.
Result is stored in file '/Users/ciprian/Downloads/abcd-tests/abcd2fiacre/tmp/test.compiled.example_portmap.Example_portmapRoot.confs'.

--------------------Verification---------------------
--------------------Warning---------------------
No warning.
[Reading confs file tmp/test.compiled.example_portmap.Example_portmapRoot.confs]
Read configurations 4 and 6 actions.
[Converting ../ABCD/examples/example_sync_chan.abcd to fiacre]
------------------------------------------------------------------
[Compiling tmp/example_sync_chan.fcr]
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/resources/test
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/classes/main/abcd2fiacre
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/resources/main
[Exploring program test.compiled.example_sync_chan.Example_sync_chanRoot]
Exploring program 'test.compiled.example_sync_chan.Example_sync_chanRoot'.
--------------------Synthesis---------------------
Explored 1 states and 1 transitions in 0 seconds.
Exploration ended normally.
Result is stored in file '/Users/ciprian/Downloads/abcd-tests/abcd2fiacre/tmp/test.compiled.example_sync_chan.Example_sync_chanRoot.confs'.

--------------------Verification---------------------
--------------------Warning---------------------
No warning.
[Reading confs file tmp/test.compiled.example_sync_chan.Example_sync_chanRoot.confs]
Read configurations 1 and 1 actions.
[Converting ../ABCD/examples/example_while.abcd to fiacre]
------------------------------------------------------------------
[Compiling tmp/example_while.fcr]
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/resources/test
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/classes/main/abcd2fiacre
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/resources/main
[Exploring program test.compiled.example_while.Example_whileRoot]
Exploring program 'test.compiled.example_while.Example_whileRoot'.
--------------------Synthesis---------------------
Explored 2 states and 2 transitions in 0.001 seconds.
Exploration ended normally.
Result is stored in file '/Users/ciprian/Downloads/abcd-tests/abcd2fiacre/tmp/test.compiled.example_while.Example_whileRoot.confs'.

--------------------Verification---------------------
--------------------Warning---------------------
Final states: 1

[Reading confs file tmp/test.compiled.example_while.Example_whileRoot.confs]
Read configurations 2 and 2 actions.
[Converting ../ABCD/examples/timer_api.abcd to fiacre]
------------------------------------------------------------------
[Compiling tmp/timer_api.fcr]
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/resources/test
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/classes/main/abcd2fiacre
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/resources/main
[Exploring program test.compiled.timer_api.Timer_apiRoot]
Exploring program 'test.compiled.timer_api.Timer_apiRoot'.
--------------------Synthesis---------------------
Explored 11 states and 11 transitions in 0.001 seconds.
Exploration ended normally.
Result is stored in file '/Users/ciprian/Downloads/abcd-tests/abcd2fiacre/tmp/test.compiled.timer_api.Timer_apiRoot.confs'.

--------------------Verification---------------------
--------------------Warning---------------------
No warning.
[Reading confs file tmp/test.compiled.timer_api.Timer_apiRoot.confs]
Read configurations 11 and 11 actions.
[Converting ../ABCD/examples/timer_api_local.abcd to fiacre]
------------------------------------------------------------------
[Compiling tmp/timer_api_local.fcr]
[Converting ../ABCD/examples/timer_api_shared.abcd to fiacre]
------------------------------------------------------------------
[Compiling tmp/timer_api_shared.fcr]
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/resources/test
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/classes/main/abcd2fiacre
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/resources/main
[Exploring program test.compiled.timer_api_shared.Timer_api_sharedRoot]
Exploring program 'test.compiled.timer_api_shared.Timer_api_sharedRoot'.
--------------------Synthesis---------------------
Explored 39 states and 46 transitions in 0.003 seconds.
Exploration ended normally.
Result is stored in file '/Users/ciprian/Downloads/abcd-tests/abcd2fiacre/tmp/test.compiled.timer_api_shared.Timer_api_sharedRoot.confs'.

--------------------Verification---------------------
--------------------Warning---------------------
No warning.
[Reading confs file tmp/test.compiled.timer_api_shared.Timer_api_sharedRoot.confs]
Read configurations 39 and 46 actions.
[Converting ../ABCD/examples/timer_flat.abcd to fiacre]
------------------------------------------------------------------
[Compiling tmp/timer_flat.fcr]
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/resources/test
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/classes/main/abcd2fiacre
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/resources/main
[Exploring program test.compiled.timer_flat.Timer_flatRoot]
Exploring program 'test.compiled.timer_flat.Timer_flatRoot'.
--------------------Synthesis---------------------
Explored 58 states and 100 transitions in 0.004 seconds.
Exploration ended normally.
Result is stored in file '/Users/ciprian/Downloads/abcd-tests/abcd2fiacre/tmp/test.compiled.timer_flat.Timer_flatRoot.confs'.

--------------------Verification---------------------
--------------------Warning---------------------
No warning.
[Reading confs file tmp/test.compiled.timer_flat.Timer_flatRoot.confs]
Read configurations 58 and 100 actions.
[Converting ../ABCD/examples/timer_shared.abcd to fiacre]
------------------------------------------------------------------
[Compiling tmp/timer_shared.fcr]
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/resources/test
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/classes/main/abcd2fiacre
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/resources/main
[Exploring program test.compiled.timer_shared.Timer_sharedRoot]
Exploring program 'test.compiled.timer_shared.Timer_sharedRoot'.
--------------------Synthesis---------------------
Explored 3 states and 2 transitions in 0.001 seconds.
Exploration ended normally.
Result is stored in file '/Users/ciprian/Downloads/abcd-tests/abcd2fiacre/tmp/test.compiled.timer_shared.Timer_sharedRoot.confs'.

--------------------Verification---------------------
--------------------Warning---------------------
Final states: 2

[Reading confs file tmp/test.compiled.timer_shared.Timer_sharedRoot.confs]
Read configurations 3 and 2 actions.
[Converting ../ABCD/examples/example1-RW.abcd to fiacre]
------------------------------------------------------------------
[Compiling tmp/example1_RW.fcr]
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/resources/test
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/classes/main/abcd2fiacre
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/resources/main
[Exploring program test.compiled.example1_rw.Example1_RWRoot]
Exploring program 'test.compiled.example1_rw.Example1_RWRoot'.
--------------------Synthesis---------------------
Explored 23 states and 23 transitions in 0.002 seconds.
Exploration ended normally.
Result is stored in file '/Users/ciprian/Downloads/abcd-tests/abcd2fiacre/tmp/test.compiled.example1_rw.Example1_RWRoot.confs'.

--------------------Verification---------------------
--------------------Warning---------------------
No warning.
[Reading confs file tmp/test.compiled.example1_rw.Example1_RWRoot.confs]
Read configurations 23 and 23 actions.
[Converting ../ABCD/examples/example11-par.abcd to fiacre]
------------------------------------------------------------------
[Compiling tmp/example11_par.fcr]
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/resources/test
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/classes/main/abcd2fiacre
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/resources/main
[Exploring program test.compiled.example11_par.Example11_parRoot]
Exploring program 'test.compiled.example11_par.Example11_parRoot'.
--------------------Synthesis---------------------
Explored 1 states and 5 transitions in 0 seconds.
Exploration ended normally.
Result is stored in file '/Users/ciprian/Downloads/abcd-tests/abcd2fiacre/tmp/test.compiled.example11_par.Example11_parRoot.confs'.

--------------------Verification---------------------
--------------------Warning---------------------
Final states: 0

[Reading confs file tmp/test.compiled.example11_par.Example11_parRoot.confs]
Read configurations 1 and 5 actions.
[Converting ../ABCD/examples/example12-min.abcd to fiacre]
------------------------------------------------------------------
[Compiling tmp/example12_min.fcr]
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/resources/test
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/classes/main/abcd2fiacre
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/resources/main
[Exploring program test.compiled.example12_min.Example12_minRoot]
Exploring program 'test.compiled.example12_min.Example12_minRoot'.
--------------------Synthesis---------------------
Explored 1,001 states and 1,000 transitions in 0.006 seconds.
Exploration ended normally.
Result is stored in file '/Users/ciprian/Downloads/abcd-tests/abcd2fiacre/tmp/test.compiled.example12_min.Example12_minRoot.confs'.

--------------------Verification---------------------
--------------------Warning---------------------
Final states: 1000

[Reading confs file tmp/test.compiled.example12_min.Example12_minRoot.confs]
Read configurations 1001 and 1000 actions.
[Converting ../ABCD/examples/example13-send_receive.abcd to fiacre]
------------------------------------------------------------------
[Compiling tmp/example13_send_receive.fcr]
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/resources/test
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/classes/main/abcd2fiacre
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/resources/main
[Exploring program test.compiled.example13_send_receive.Example13_send_receiveRoot]
Exploring program 'test.compiled.example13_send_receive.Example13_send_receiveRoot'.
--------------------Synthesis---------------------
Explored 12 states and 11 transitions in 0.001 seconds.
Exploration ended normally.
Result is stored in file '/Users/ciprian/Downloads/abcd-tests/abcd2fiacre/tmp/test.compiled.example13_send_receive.Example13_send_receiveRoot.confs'.

--------------------Verification---------------------
--------------------Warning---------------------
Final states: 11

[Reading confs file tmp/test.compiled.example13_send_receive.Example13_send_receiveRoot.confs]
Read configurations 12 and 11 actions.
[Converting ../ABCD/examples/example14-counter.abcd to fiacre]
------------------------------------------------------------------
[Compiling tmp/example14_counter.fcr]
[Converting ../ABCD/examples/example15_multicoms.abcd to fiacre]
------------------------------------------------------------------
[Compiling tmp/example15_multicoms.fcr]
[Converting ../ABCD/examples/example16_local_mutex.abcd to fiacre]
WARNING: local mutex 'm' in process p will be removed
------------------------------------------------------------------
[Compiling tmp/example16_local_mutex.fcr]
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/resources/test
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/classes/main/abcd2fiacre
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/resources/main
[Exploring program test.compiled.example16_local_mutex.Example16_local_mutexRoot]
Exploring program 'test.compiled.example16_local_mutex.Example16_local_mutexRoot'.
--------------------Synthesis---------------------
Explored 16 states and 32 transitions in 0.001 seconds.
Exploration ended normally.
Result is stored in file '/Users/ciprian/Downloads/abcd-tests/abcd2fiacre/tmp/test.compiled.example16_local_mutex.Example16_local_mutexRoot.confs'.

--------------------Verification---------------------
--------------------Warning---------------------
Final states: 15

[Reading confs file tmp/test.compiled.example16_local_mutex.Example16_local_mutexRoot.confs]
Read configurations 16 and 32 actions.
[Converting ../ABCD/examples/example16_mutex.abcd to fiacre]
------------------------------------------------------------------
[Compiling tmp/example16_mutex.fcr]
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/resources/test
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/classes/main/abcd2fiacre
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/resources/main
[Exploring program test.compiled.example16_mutex.Example16_mutexRoot]
Exploring program 'test.compiled.example16_mutex.Example16_mutexRoot'.
--------------------Synthesis---------------------
Explored 384 states and 2,880 transitions in 0.018 seconds.
Exploration ended normally.
Result is stored in file '/Users/ciprian/Downloads/abcd-tests/abcd2fiacre/tmp/test.compiled.example16_mutex.Example16_mutexRoot.confs'.

--------------------Verification---------------------
--------------------Warning---------------------
Final states: 383

[Reading confs file tmp/test.compiled.example16_mutex.Example16_mutexRoot.confs]
Read configurations 384 and 2880 actions.
[Converting ../ABCD/examples/example16_nolock_mutex.abcd to fiacre]
WARNING: Process v tries to unlocks mutex 'm' but it never locks it
------------------------------------------------------------------
[Compiling tmp/example16_nolock_mutex.fcr]
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/resources/test
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/classes/main/abcd2fiacre
incorrect classpath: /Users/ciprian/Downloads/abcd-tests/build/resources/main
[Exploring program test.compiled.example16_nolock_mutex.Example16_nolock_mutexRoot]
Exploring program 'test.compiled.example16_nolock_mutex.Example16_nolock_mutexRoot'.
--------------------Synthesis---------------------
Explored 1 states and 1 transitions in 0 seconds.
Exploration ended normally.
Result is stored in file '/Users/ciprian/Downloads/abcd-tests/abcd2fiacre/tmp/test.compiled.example16_nolock_mutex.Example16_nolock_mutexRoot.confs'.

--------------------Verification---------------------
--------------------Warning---------------------
Final states: 0

[Reading confs file tmp/test.compiled.example16_nolock_mutex.Example16_nolock_mutexRoot.confs]
Read configurations 1 and 1 actions.

Standard error

Exploration with: BFSExplorer
The DBM has 0 clocks
Exploration with: BFSExplorer
The DBM has 0 clocks
Exploration with: BFSExplorer
The DBM has 0 clocks
Exploration with: BFSExplorer
The DBM has 0 clocks
Exploration with: BFSExplorer
The DBM has 0 clocks
Exploration with: BFSExplorer
The DBM has 0 clocks
Exploration with: BFSExplorer
The DBM has 0 clocks
Exploration with: BFSExplorer
The DBM has 0 clocks
Exploration with: BFSExplorer
The DBM has 0 clocks
Exploration with: BFSExplorer
The DBM has 0 clocks
Exploration with: BFSExplorer
The DBM has 3 clocks
Exploration with: BFSExplorer
The DBM has 2 clocks
Exploration with: BFSExplorer
The DBM has 0 clocks
Exploration with: BFSExplorer
The DBM has 0 clocks
Exploration with: BFSExplorer
The DBM has 0 clocks
Exploration with: BFSExplorer
The DBM has 0 clocks
Exploration with: BFSExplorer
The DBM has 0 clocks
Syntax error on token 'none', line 4 column 19.
Exploration with: BFSExplorer
The DBM has 0 clocks
Exploration with: BFSExplorer
The DBM has 0 clocks
Exploration with: BFSExplorer
The DBM has 0 clocks
Exploration with: BFSExplorer
The DBM has 0 clocks
Exploration with: BFSExplorer
The DBM has 0 clocks
Exploration with: BFSExplorer
The DBM has 0 clocks
Exploration with: BFSExplorer
The DBM has 0 clocks
Exploration with: BFSExplorer
The DBM has 0 clocks
Exploration with: BFSExplorer
The DBM has 2 clocks
In component 'main', port 'vStart0' isn't used.

Exploration with: BFSExplorer
The DBM has 2 clocks
Exploration with: BFSExplorer
The DBM has 3 clocks
Exploration with: BFSExplorer
The DBM has 2 clocks
Exploration with: BFSExplorer
The DBM has 0 clocks
Exploration with: BFSExplorer
The DBM has 0 clocks
Exploration with: BFSExplorer
The DBM has 0 clocks
Exploration with: BFSExplorer
The DBM has 0 clocks
Can't find reference for element named 'result' in null.
Exploration with: BFSExplorer
The DBM has 0 clocks
Exploration with: BFSExplorer
The DBM has 0 clocks
Exploration with: BFSExplorer
The DBM has 0 clocks