From: Marion Guthmuller Date: Wed, 5 Dec 2012 14:58:31 +0000 (+0100) Subject: model-checker : update snapshot_comparison tests X-Git-Tag: v3_9_rc1~86^2~184^2~9 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/d28deecd8877f863c3b2f8623da62ce8aeee304c model-checker : update snapshot_comparison tests --- diff --git a/examples/msg/mc/test/snapshot_comparison1.c b/examples/msg/mc/test/snapshot_comparison1.c index 982b1466ee..126c590243 100644 --- a/examples/msg/mc/test/snapshot_comparison1.c +++ b/examples/msg/mc/test/snapshot_comparison1.c @@ -35,7 +35,7 @@ int test(int argc, char **argv){ XBT_INFO("**** End test ****"); - return 0; + xbt_abort(); } int main(int argc, char **argv){ diff --git a/examples/msg/mc/test/snapshot_comparison1.tesh b/examples/msg/mc/test/snapshot_comparison1.tesh index 8e2dc36b1a..eafc8c6be5 100644 --- a/examples/msg/mc/test/snapshot_comparison1.tesh +++ b/examples/msg/mc/test/snapshot_comparison1.tesh @@ -2,25 +2,13 @@ ! expect signal SIGABRT ! timeout 200 -$ ${bindir:=.}/snapshot_comparison1 --cfg=model-check:1 --cfg=contexts/factory:ucontext "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" +$ ${bindir:=.}/snapshot_comparison1 --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) Take two successive snapshots (No modification) -> [ 1.000000] (1:test@HostA) First snapshot -> [ 3.000000] (1:test@HostA) Second snapshot -> [ 3.000000] (1:test@HostA) Test result : 0 (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 +> [ 0.000000] (1:test@HostA) **** Start test **** +> [ 0.000000] (1:test@HostA) Take two successive snapshots (No modification) +> [ 0.000000] (1:test@HostA) First snapshot +> [ 0.000000] (1:test@HostA) Second snapshot +> [ 0.000000] (1:test@HostA) Test result : 0 (0 = state equality, 1 = different states) +> [ 0.000000] (1:test@HostA) **** End test **** diff --git a/examples/msg/mc/test/snapshot_comparison2.c b/examples/msg/mc/test/snapshot_comparison2.c index e3b04b03e4..9c08973e5c 100644 --- a/examples/msg/mc/test/snapshot_comparison2.c +++ b/examples/msg/mc/test/snapshot_comparison2.c @@ -40,7 +40,7 @@ int test(int argc, char **argv){ xbt_free(toto); - return 0; + xbt_abort(); } int main(int argc, char **argv){ diff --git a/examples/msg/mc/test/snapshot_comparison2.tesh b/examples/msg/mc/test/snapshot_comparison2.tesh index 8e3798c2d8..c383fd2f81 100644 --- a/examples/msg/mc/test/snapshot_comparison2.tesh +++ b/examples/msg/mc/test/snapshot_comparison2.tesh @@ -6,22 +6,10 @@ $ ${bindir:=.}/snapshot_comparison2 --cfg=model-check:1 "--log=root.fmt:[%10.6r] > [ 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) Malloc after first snapshot -> [ 2.000000] (1:test@HostA) First snapshot -> [ 2.000000] (1:test@HostA) Toto allocated -> [ 3.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 +> [ 0.000000] (1:test@HostA) **** Start test **** +> [ 0.000000] (1:test@HostA) Malloc after first snapshot +> [ 0.000000] (1:test@HostA) First snapshot +> [ 0.000000] (1:test@HostA) Toto allocated +> [ 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 **** diff --git a/examples/msg/mc/test/snapshot_comparison3.c b/examples/msg/mc/test/snapshot_comparison3.c index 8c3efd3a67..e46578fe99 100644 --- a/examples/msg/mc/test/snapshot_comparison3.c +++ b/examples/msg/mc/test/snapshot_comparison3.c @@ -46,7 +46,7 @@ int test(int argc, char **argv){ XBT_INFO("**** End test ****"); - return 0; + xbt_abort(); } int main(int argc, char **argv){ diff --git a/examples/msg/mc/test/snapshot_comparison3.tesh b/examples/msg/mc/test/snapshot_comparison3.tesh index 37a7635651..806106b2db 100644 --- a/examples/msg/mc/test/snapshot_comparison3.tesh +++ b/examples/msg/mc/test/snapshot_comparison3.tesh @@ -6,23 +6,11 @@ $ ${bindir:=.}/snapshot_comparison3 --cfg=model-check:1 "--log=root.fmt:[%10.6r] > [ 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) Malloc and free after first snapshot -> [ 2.000000] (1:test@HostA) First snapshot -> [ 2.000000] (1:test@HostA) Toto allocated -> [ 2.000000] (1:test@HostA) Toto free -> [ 3.000000] (1:test@HostA) Second snapshot -> [ 3.000000] (1:test@HostA) Test result : 0 (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 +> [ 0.000000] (1:test@HostA) **** Start test **** +> [ 0.000000] (1:test@HostA) Malloc and free after first snapshot +> [ 0.000000] (1:test@HostA) First snapshot +> [ 0.000000] (1:test@HostA) Toto allocated +> [ 0.000000] (1:test@HostA) Toto free +> [ 0.000000] (1:test@HostA) Second snapshot +> [ 0.000000] (1:test@HostA) Test result : 0 (0 = state equality, 1 = different states) +> [ 0.000000] (1:test@HostA) **** End test **** diff --git a/examples/msg/mc/test/snapshot_comparison4.c b/examples/msg/mc/test/snapshot_comparison4.c index e87c65c0ce..bff95bfe0a 100644 --- a/examples/msg/mc/test/snapshot_comparison4.c +++ b/examples/msg/mc/test/snapshot_comparison4.c @@ -44,7 +44,7 @@ int test(int argc, char **argv){ XBT_INFO("**** End test ****"); - return 0; + xbt_abort(); } int main(int argc, char **argv){ diff --git a/examples/msg/mc/test/snapshot_comparison4.tesh b/examples/msg/mc/test/snapshot_comparison4.tesh index ba6fec7f6f..05db501811 100644 --- a/examples/msg/mc/test/snapshot_comparison4.tesh +++ b/examples/msg/mc/test/snapshot_comparison4.tesh @@ -6,23 +6,11 @@ $ ${bindir:=.}/snapshot_comparison4 --cfg=model-check:1 "--log=root.fmt:[%10.6r] > [ 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 diff --git a/examples/msg/mc/test/snapshot_comparison5.c b/examples/msg/mc/test/snapshot_comparison5.c index eef83c8651..307885419a 100644 --- a/examples/msg/mc/test/snapshot_comparison5.c +++ b/examples/msg/mc/test/snapshot_comparison5.c @@ -44,7 +44,7 @@ int test(int argc, char **argv){ XBT_INFO("**** End test ****"); - return 0; + xbt_abort(); } int main(int argc, char **argv){ diff --git a/examples/msg/mc/test/snapshot_comparison5.tesh b/examples/msg/mc/test/snapshot_comparison5.tesh index 010ab35faa..bfed346930 100644 --- a/examples/msg/mc/test/snapshot_comparison5.tesh +++ b/examples/msg/mc/test/snapshot_comparison5.tesh @@ -6,23 +6,11 @@ $ ${bindir:=.}/snapshot_comparison5 --cfg=model-check:1 "--log=root.fmt:[%10.6r] > [ 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) Increment local variable -> [ 1.000000] (1:test@HostA) j = 0 -> [ 2.000000] (1:test@HostA) First snapshot -> [ 2.000000] (1:test@HostA) j = 1 -> [ 3.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 +> [ 0.000000] (1:test@HostA) **** Start test **** +> [ 0.000000] (1:test@HostA) Increment local variable +> [ 0.000000] (1:test@HostA) j = 0 +> [ 0.000000] (1:test@HostA) First snapshot +> [ 0.000000] (1:test@HostA) j = 1 +> [ 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 ****