Class org.cte.ABCD.fiacre.tests.ABCDBaseExplorationTest
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