diff options
author | qadeer <unknown> | 2014-05-03 10:06:13 -0700 |
---|---|---|
committer | qadeer <unknown> | 2014-05-03 10:06:13 -0700 |
commit | 36e016acf963b7c19d59640b11b4a40f2072943e (patch) | |
tree | 31a45e868059d0ffe54fc3d212261245ff97886a /Test/og/parallel1.bpl | |
parent | 121071b9f87d23eaeba176897b9655cd540fb694 (diff) |
checkpoint
Diffstat (limited to 'Test/og/parallel1.bpl')
-rw-r--r-- | Test/og/parallel1.bpl | 36 |
1 files changed, 25 insertions, 11 deletions
diff --git a/Test/og/parallel1.bpl b/Test/og/parallel1.bpl index fc33d6cc..18050e09 100644 --- a/Test/og/parallel1.bpl +++ b/Test/og/parallel1.bpl @@ -1,27 +1,41 @@ -var g:int;
+var {:phase 1} g:int;
-procedure {:yields} {:stable} PB()
-modifies g;
+procedure {:yields} {:phase 1} PB()
{
- g := g + 1;
+ yield;
+ call Incr();
+ yield;
}
-procedure {:yields} {:stable} PC()
-ensures g == 3;
+procedure {:yields} {:phase 0,1} Incr();
+ensures {:atomic}
+|{A:
+ g := g + 1; return true;
+}|;
+
+procedure {:yields} {:phase 0,1} Set(v: int);
+ensures {:atomic}
+|{A:
+ g := v; return true;
+}|;
+
+procedure {:yields} {:phase 1} PC()
+ensures {:phase 1} g == 3;
{
- g := 3;
yield;
- assert g == 3;
+ call Set(3);
+ yield;
+ assert {:phase 1} g == 3;
}
-procedure {:yields} {:stable} PD()
+procedure {:yields} {:phase 1} PD()
{
call PC();
- assert g == 3;
+ assert {:phase 1} g == 3;
yield;
}
-procedure {:entrypoint} {:yields} Main()
+procedure {:yields} {:phase 1} Main()
{
while (true)
{
|