Finished fairness implementation and test suite

benchmarks/temporal/cade/AFAGBranch.ctl

@@ -0,0 +1,24 @@
+fields: next;
+precondition: current=four * x=zero * zero->one * one->two * two->three * three->four * four->five * FALSE->false' * TRUE->true' * break=FALSE;
+property: AF(AG(x=one));
+while break=FALSE do
+  if current=five then
+    break:=TRUE
+  else
+    if * then
+      current:=current.next
+    else
+      current:=five
+    fi
+  fi
+od;
+while TRUE=TRUE do
+  if * then
+    x:=one
+  else
+    x:=one
+  fi
+od;
+while TRUE=TRUE do
+  skip
+od

benchmarks/temporal/cade/AFEFBranch.ctl

@@ -0,0 +1,27 @@
+fields: next;
+precondition: current=four * x=zero * zero->one * one->two * two->three * three->four * four->five * FALSE->false' * TRUE->true' * break=FALSE;
+property: AF(EF(x=one));
+while break=FALSE do
+  if current=five then
+    break:=TRUE
+  else
+    current:=current.next
+  fi
+od;
+break:=FALSE;
+current:=four;
+while break=FALSE do
+  if current=five then
+    break:=TRUE
+  else
+    if * then
+      current:=current.next
+    else
+      current:=current.next
+    fi
+  fi
+od;
+x:=one;
+while TRUE=TRUE do
+  skip
+od

benchmarks/temporal/cade/AGImpEFBranch.ctl

@@ -0,0 +1,20 @@
+fields: next;
+precondition: current=four * check=zero * p=zero * zero->one * one->two * two->three * three->four * four->five * FALSE->false' * TRUE->true' * break=FALSE;
+property: AG(\/(check=zero,EF(p=one)));
+check:=one;
+while break=FALSE do
+  if current=five then
+    break:=TRUE
+  else
+    check:=one;
+    if * then
+      current:=current.next
+    else
+      skip
+    fi
+  fi
+od;
+p:=one;
+while TRUE=TRUE do
+  skip
+od

benchmarks/temporal/cade/AGImpEGBranch.ctl

@@ -0,0 +1,11 @@
+fields: next;
+precondition: current=zero * check=zero * p=one * zero->one * one->nil  * FALSE->false' * TRUE->true';
+property: AG(\/(check=zero,EG(p=one)));
+while TRUE=TRUE do
+  check:=one;
+  if * then
+    p:=one
+  else
+    p:=one
+  fi
+od

benchmarks/temporal/cade/Acq-rel3.ctl

@@ -0,0 +1,29 @@
+fields: next;
+precondition: a=nil * r=nil * flag->f' * x->x' * three->two * two->one * one->nil;
+property: /\(EF(a!=nil),EF(AG(r=nil)));
+while flag!=nil do
+    if * then
+	free(flag);
+        flag:=nil
+    else
+	skip
+    fi;
+    if flag!=nil then
+	x:=new();
+	x.next:=three;
+        a:=new();
+	free(a);
+	a:=nil;
+	while x=x do
+	    skip
+	od;
+	r:=new();
+	free(r);
+	r:=nil
+    else
+	skip
+    fi
+od;
+while flag=flag do
+    skip
+od

benchmarks/temporal/cade/Acq-rel4.ctl

@@ -0,0 +1,29 @@
+fields: next;
+precondition: a=nil * r=nil * flag->f' * x->x' * three->two * two->one * one->nil;
+property: AF(AG(r=nil));
+while flag!=nil do
+    if * then
+	free(flag);
+        flag:=nil
+    else
+	skip
+    fi;
+    if flag!=nil then
+	x:=new();
+	x.next:=three;
+        a:=new();
+	free(a);
+	a:=nil;
+	while x=x do
+	    skip
+	od;
+	r:=new();
+	free(r);
+	r:=nil
+    else
+	skip
+    fi
+od;
+while flag=flag do
+    skip
+od

benchmarks/temporal/cade/Acq-rel5.ctl

@@ -0,0 +1,29 @@
+fields: next;
+precondition: a=nil * r=nil * flag->f' * x->x' * three->two * two->one * one->nil;
+property: /\(EF(a!=nil),EF(EG(r=nil)));
+while flag!=nil do
+    if * then
+	free(flag);
+        flag:=nil
+    else
+	skip
+    fi;
+    if flag!=nil then
+	x:=new();
+	x.next:=three;
+        a:=new();
+	free(a);
+	a:=nil;
+	while x!=nil do
+	    x:=x.next
+	od;
+	r:=new();
+	free(r);
+	r:=nil
+    else
+	skip
+    fi
+od;
+while flag=flag do
+    skip
+od

benchmarks/temporal/cade/Acq-rel6.ctl

@@ -0,0 +1,29 @@
+fields: next;
+precondition: a=nil * r=nil * flag->f' * x->x' * three->two * two->one * one->nil;
+property: AF(EG(r=nil));
+while flag!=nil do
+    if * then
+	free(flag);
+        flag:=nil
+    else
+	skip
+    fi;
+    if flag!=nil then
+	x:=new();
+	x.next:=three;
+        a:=new();
+	free(a);
+	a:=nil;
+	while x!=nil do
+	    x:=x.next
+	od;
+	r:=new();
+	free(r);
+	r:=nil
+    else
+	skip
+    fi
+od;
+while flag=flag do
+    skip
+od

benchmarks/temporal/cade/Cyclic-List1.ctl

@@ -0,0 +1,6 @@
+fields: next;
+precondition: List(x,x);
+property: AG(List(x,x));
+while x=x do
+x:=x.next
+od

benchmarks/temporal/cade/Cyclic-List2.ctl

@@ -0,0 +1,6 @@
+fields: next;
+precondition: List(x,x);
+property: AG(EG(List(x,x)));
+while x=x do
+x:=x.next
+od

benchmarks/temporal/cade/EGAFBranch.ctl

@@ -0,0 +1,18 @@
+fields: next;
+precondition: current=zero * x=zero * zero->one * one->two * two->three * three->four * four->five * FALSE->false' * TRUE->true' * break=FALSE;
+property: EG(AF(x=one));
+if * then
+  while break=FALSE do 
+    if current=five then
+      break:=TRUE
+    else
+      current:=current.next
+    fi
+  od;
+  x:=one
+else
+  x:=one
+fi;
+while TRUE=TRUE do
+  skip
+od

benchmarks/temporal/cade/EGAGBranch.ctl

@@ -0,0 +1,11 @@
+fields: next;
+precondition: x=one * zero->one * one->two * two->three * three->four * four->five * TRUE->true';
+property: EG(AG(x=one));
+if * then
+  x:=one
+else
+  skip
+fi;
+while TRUE=TRUE do
+  skip
+od

benchmarks/temporal/cade/EGImpAFBranch.ctl

@@ -0,0 +1,18 @@
+fields: next;
+precondition: current=four * check=zero * p=zero * zero->one * one->two * two->three * three->four * four->five * FALSE->false' * TRUE->true' * break=FALSE;
+property: EG(\/(x=zero,AF(p=one)));
+while TRUE=TRUE do
+  check:=zero.next;
+  if * then
+    while break=FALSE do
+      if current=five then
+        break:=TRUE
+      else
+	  current:=current.next
+      fi
+    od;
+    p:=one
+  else
+    p:=zero
+  fi
+od

benchmarks/temporal/cade/EGImpEFBranch.ctl

@@ -0,0 +1,23 @@
+fields: next;
+precondition: current=four * check=zero * p=zero * zero->one * one->two * two->three * three->four * four->five * FALSE->false' * TRUE->true' * break=FALSE;
+property: EG(\/(x=zero,EF(p=one)));
+while TRUE=TRUE do
+  check:=zero.next;
+  if * then
+    while break=FALSE do
+      if current=five then
+        break:=TRUE
+      else
+        if * then
+	  current:=current.next
+	else
+	  current:=current.next;
+	  current:=current.next
+	fi
+      fi
+    od;
+    p:=one
+  else
+    p:=zero
+  fi
+od

benchmarks/temporal/cade/Fin-Lock1.ctl

@@ -0,0 +1,10 @@
+fields: next;
+precondition: a->zero * r->zero * ls(x,nil);
+property:AF(a->one * r->one * emp);
+a.next:=one;
+while x!=nil do
+      temp:=x;
+      x:=x.next;
+      free(temp)
+od;
+r.next:=one

benchmarks/temporal/cade/Fin-Lock2.ctl

@@ -0,0 +1,10 @@
+fields: next;
+precondition: a->zero * r->zero * ls(x,nil);
+property:AG(AF(a->one * r->one * emp));
+a.next:=one;
+while x!=nil do
+      temp:=x;
+      x:=x.next;
+      free(temp)
+od;
+r.next:=one

benchmarks/temporal/cade/Fin-Lock3.ctl

@@ -0,0 +1,10 @@
+fields: next;
+precondition: lock->zero * ls(x,nil);
+property:AG(AF(/\(lock->one * emp,<>lock->one)));
+lock.next:=one;
+while x!=nil do
+      temp:=x;
+      x:=x.next;
+      free(temp)
+od;
+lock.next:=zero

benchmarks/temporal/cade/Inf-BinTree.ctl

@@ -0,0 +1,9 @@
+fields: left,right;
+precondition: x!=nil * bt(x);
+property: AG(EG(x!=nil));
+while x=x do
+    temp:=new();
+    temp.left:=x;
+    temp.right:=nil;
+    x:=temp
+od

benchmarks/temporal/cade/Inf-List1.ctl

@@ -0,0 +1,12 @@
+fields: next;
+precondition: ls(y',x) * ls(x,nil);
+property: AG(ls(y',x) * ls(x,nil));
+while x=x do
+    if x!= nil then
+      temp:=x;
+      x := x.next;
+      temp:=nil
+    else
+      skip
+    fi
+od

benchmarks/temporal/cade/Inf-Lock1.ctl

@@ -0,0 +1,13 @@
+fields: next;
+precondition: flag=false * a->zero * r->zero * ls(x,nil);
+property:AG(AF(a->one * r->one * emp));
+while x=x do
+flag:=true;
+a.next:=one;
+while x!=nil do
+      temp:=x;
+      x:=x.next;
+      free(temp)
+od;
+r.next:=one
+od

benchmarks/temporal/cade/Inf-Lock2.ctl

@@ -0,0 +1,12 @@
+fields: next;
+precondition: lock->zero * ls(x,nil);
+property:AG(AF(/\(lock->one * emp,<>lock->one)));
+while x=x do
+lock.next:=one;
+while x!=nil do
+      temp:=x;
+      x:=x.next;
+      free(temp)
+od;
+lock.next:=zero
+od