From 4d089806a414eaecd252aed471fd4adc90d591b2 Mon Sep 17 00:00:00 2001 From: Namratha Date: Sun, 28 Apr 2024 01:06:58 +0200 Subject: [PATCH] layer fixes --- Test/civl/samples/snapshot.bpl | 34 +++++++++++++++++----------------- 1 file changed, 17 insertions(+), 17 deletions(-) diff --git a/Test/civl/samples/snapshot.bpl b/Test/civl/samples/snapshot.bpl index 10ae680b1..11f5f8d21 100644 --- a/Test/civl/samples/snapshot.bpl +++ b/Test/civl/samples/snapshot.bpl @@ -63,22 +63,6 @@ refines scan'; } } -atomic action {:layer 2} write (v:Value, i: int) -modifies mem; -{ - var x: StampedValue; - x := mem[i]; - mem[i] := StampedValue(x->ts + 1, v); -} - -action {:layer 1} action_read (i: int) returns (v: StampedValue) -{ - v := mem[i]; -} - -yield procedure {:layer 0} read (i: int) returns (v: StampedValue); -refines action_read; - right action {:layer 2} action_read_f (i: int) returns (out: StampedValue) { var {:pool "K"} k:int; @@ -116,4 +100,20 @@ yield procedure {:layer 1} read_s (i: int) returns (out: StampedValue) refines action_read_s; { call out := read(i); -} \ No newline at end of file +} + +atomic action {:layer 1,3} action_write (v:Value, i: int) +modifies mem; +{ + var x: StampedValue; + x := mem[i]; + mem[i] := StampedValue(x->ts + 1, v); +} + +action {:layer 1,3} action_read (i: int) returns (v: StampedValue) +{ + v := mem[i]; +} + +yield procedure {:layer 0} read (i: int) returns (v: StampedValue); +refines action_read; \ No newline at end of file