X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/e4abd3f271729beeff499da36267bfb274dd1f6d..0c13871d73e933c1847faf8debea7b7745a3ff44:/examples/msg/mc/test/snapshot_comparison4.tesh diff --git a/examples/msg/mc/test/snapshot_comparison4.tesh b/examples/msg/mc/test/snapshot_comparison4.tesh index 146d2b8bc0..6f4ca6546d 100644 --- a/examples/msg/mc/test/snapshot_comparison4.tesh +++ b/examples/msg/mc/test/snapshot_comparison4.tesh @@ -1,28 +1,15 @@ #! ./tesh ! expect signal SIGABRT -! timeout 120 +! timeout 200 $ ${bindir:=.}/snapshot_comparison4 --cfg=model-check:1 "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" > [ 0.000000] (0:@) Configuration change: Set 'model-check' to '1' -> [ 0.000000] (0:@) type in variable = 2 > [ 0.000000] (0:@) Check the liveness property promela -> [ 1.000000] (1:test@HostA) **** Start test **** -> [ 1.000000] (1:test@HostA) Free after first snapshot -> [ 1.000000] (1:test@HostA) Toto allocated -> [ 2.000000] (1:test@HostA) First snapshot -> [ 2.000000] (1:test@HostA) Toto free -> [ 2.000000] (1:test@HostA) Second snapshot -> [ 3.000000] (1:test@HostA) Test result : 1 (0 = state equality, 1 = different states) -> [ 3.000000] (1:test@HostA) **** End test **** -> [ 0.000000] (0:@) Next pair (depth = 5) already reached ! -> [ 0.000000] (0:@) *-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-* -> [ 0.000000] (0:@) | ACCEPTANCE CYCLE | -> [ 0.000000] (0:@) *-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-* -> [ 0.000000] (0:@) Counter-example that violates formula : -> [ 0.000000] (0:@) [(1)test] MC_SNAPSHOT ((null)) -> [ 0.000000] (0:@) [(1)test] MC_SNAPSHOT ((null)) -> [ 0.000000] (0:@) [(1)test] MC_COMPARE_SNAPSHOTS ((null)) -> [ 0.000000] (0:@) End of system requests but evolution in Büchi automaton -> [ 0.000000] (0:@) Expanded pairs = 5 -> [ 0.000000] (0:@) Visited pairs = 4 -> [ 0.000000] (0:@) Expanded / Visited = 0.800000 \ No newline at end of file +> [ 0.000000] (1:test@HostA) **** Start test **** +> [ 0.000000] (1:test@HostA) Free after first snapshot +> [ 0.000000] (1:test@HostA) Toto allocated +> [ 0.000000] (1:test@HostA) First snapshot +> [ 0.000000] (1:test@HostA) Toto free +> [ 0.000000] (1:test@HostA) Second snapshot +> [ 0.000000] (1:test@HostA) Test result : 1 (0 = state equality, 1 = different states) +> [ 0.000000] (1:test@HostA) **** End test **** \ No newline at end of file