From d0581029149ed8928e01918184f8ea115cc4f484 Mon Sep 17 00:00:00 2001 From: Marion Guthmuller Date: Thu, 10 Jan 2013 20:24:35 +0100 Subject: [PATCH] model-checker : update tesh --- examples/msg/mc/bugged1_liveness.tesh | 1 - examples/msg/mc/test/snapshot_comparison1.tesh | 1 - examples/msg/mc/test/snapshot_comparison2.tesh | 1 - examples/msg/mc/test/snapshot_comparison3.tesh | 1 - examples/msg/mc/test/snapshot_comparison4.tesh | 1 - examples/msg/mc/test/snapshot_comparison5.tesh | 1 - 6 files changed, 6 deletions(-) diff --git a/examples/msg/mc/bugged1_liveness.tesh b/examples/msg/mc/bugged1_liveness.tesh index 97ff4e7c04..ac0a2cbcd2 100644 --- a/examples/msg/mc/bugged1_liveness.tesh +++ b/examples/msg/mc/bugged1_liveness.tesh @@ -4,7 +4,6 @@ ! timeout 200 $ ${bindir:=.}/bugged1_liveness --cfg=model-check:1 --cfg=contexts/factory:ucontext "--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_bugged1_liveness > [ 0.000000] (2:client@Fafard) Ask the request > [ 0.000000] (3:client@Boivin) Ask the request diff --git a/examples/msg/mc/test/snapshot_comparison1.tesh b/examples/msg/mc/test/snapshot_comparison1.tesh index eafc8c6be5..119844a1f2 100644 --- a/examples/msg/mc/test/snapshot_comparison1.tesh +++ b/examples/msg/mc/test/snapshot_comparison1.tesh @@ -4,7 +4,6 @@ ! timeout 200 $ ${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 > [ 0.000000] (1:test@HostA) **** Start test **** > [ 0.000000] (1:test@HostA) Take two successive snapshots (No modification) diff --git a/examples/msg/mc/test/snapshot_comparison2.tesh b/examples/msg/mc/test/snapshot_comparison2.tesh index c383fd2f81..230bbcce5c 100644 --- a/examples/msg/mc/test/snapshot_comparison2.tesh +++ b/examples/msg/mc/test/snapshot_comparison2.tesh @@ -4,7 +4,6 @@ ! timeout 200 $ ${bindir:=.}/snapshot_comparison2 --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 > [ 0.000000] (1:test@HostA) **** Start test **** > [ 0.000000] (1:test@HostA) Malloc after first snapshot diff --git a/examples/msg/mc/test/snapshot_comparison3.tesh b/examples/msg/mc/test/snapshot_comparison3.tesh index 806106b2db..6589319479 100644 --- a/examples/msg/mc/test/snapshot_comparison3.tesh +++ b/examples/msg/mc/test/snapshot_comparison3.tesh @@ -4,7 +4,6 @@ ! timeout 200 $ ${bindir:=.}/snapshot_comparison3 --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 > [ 0.000000] (1:test@HostA) **** Start test **** > [ 0.000000] (1:test@HostA) Malloc and free after first snapshot diff --git a/examples/msg/mc/test/snapshot_comparison4.tesh b/examples/msg/mc/test/snapshot_comparison4.tesh index 05db501811..6f4ca6546d 100644 --- a/examples/msg/mc/test/snapshot_comparison4.tesh +++ b/examples/msg/mc/test/snapshot_comparison4.tesh @@ -4,7 +4,6 @@ ! 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 > [ 0.000000] (1:test@HostA) **** Start test **** > [ 0.000000] (1:test@HostA) Free after first snapshot diff --git a/examples/msg/mc/test/snapshot_comparison5.tesh b/examples/msg/mc/test/snapshot_comparison5.tesh index bfed346930..d483ae3c7d 100644 --- a/examples/msg/mc/test/snapshot_comparison5.tesh +++ b/examples/msg/mc/test/snapshot_comparison5.tesh @@ -4,7 +4,6 @@ ! timeout 200 $ ${bindir:=.}/snapshot_comparison5 --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 > [ 0.000000] (1:test@HostA) **** Start test **** > [ 0.000000] (1:test@HostA) Increment local variable -- 2.20.1