Adding missing files to previous commit

all.itarget

@@ -9,6 +9,7 @@ src/while/while_prove.native
 src/while/while_abduce.native
 src/extended_while/extended_while_prove.native  
 src/temporal_ctl/temporal_ctl_prove.native
+src/temporal_ctl/temporal_ctl_prove.byte
 src/temporal_ltl/temporal_ltl_prove.native
 #src/cyclist.docdir/index.html
 src/seplog/sl.top

benchmarks/temporal/cyclic_list_nd.ctl

@@ -0,0 +1,11 @@
+fields: next;
+precondition: List(x,x);
+property: AG(List(x,x));
+while x=x do
+if * then
+  x:=x.next
+else
+  y:=new();
+  y.next:=x
+fi
+od

benchmarks/temporal/fairness/test1.fctl

@@ -0,0 +1,7 @@
+fields: next;
+precondition:x=x;
+property: AF(final);
+while * do
+      skip	
+od;
+skip

benchmarks/temporal/fairness/test2.fctl

@@ -0,0 +1,7 @@
+fields: next;
+precondition:x=x;
+property: AF(final);
+while x=x do
+  skip 	
+od;
+skip

benchmarks/temporal/fairness/test3.fctl

@@ -0,0 +1,10 @@
+fields: next;
+precondition:x->x';
+property: AF(emp);
+while x=x do
+  if * then
+     free(x)
+  else
+     skip
+  fi
+od

benchmarks/temporal/fairness/test4.fctl

@@ -0,0 +1,12 @@
+fields: next;
+precondition:x->x';
+property: AF(emp);
+while x=x do
+  if * then
+     free(x)
+  else
+     while * do
+       skip
+     od
+  fi
+od

benchmarks/temporal/fairness/test5.fctl

@@ -0,0 +1,14 @@
+fields: next;
+precondition: tmp->x * ls(x,nil);
+property: AF(emp);
+while x=x do
+  if * then
+     while tmp!=nil do
+	free(tmp);
+	tmp:= x;
+	x:= x.next
+     od
+  else
+     skip
+  fi
+od

benchmarks/temporal/fairness/test6.fctl

@@ -0,0 +1,16 @@
+fields: next;
+precondition: ls(x,nil);
+property: AF(emp);
+while x=x do
+  if * then
+     while x!=nil do
+       temp:=x.next;
+       free(x);
+       x:=temp
+     od
+  else
+    while * do
+       skip
+     od	
+  fi
+od

benchmarks/temporal/fairness/test7.fctl

@@ -0,0 +1,18 @@
+fields: next;
+precondition: ls(x,nil);
+property: AF(emp);
+while x=x do
+  if * then
+     while x!=nil do
+       temp:=x.next;
+       free(x);
+       x:=temp
+     od
+  else
+    while * do
+       y:=new();
+       y.next:=x;
+       x:=y
+     od	
+  fi
+od

benchmarks/temporal/fairness/test8.fctl

@@ -0,0 +1,19 @@
+fields: next;
+precondition: ls(x,nil);
+property: AG(AF(emp));
+while x=x do
+  if * then
+     while x!=nil do
+       temp:=x;
+       x:=x.next;
+       free(temp);
+       temp:=nil
+     od
+  else
+    while * do
+       y:=new();
+       y.next:=x;
+       x:=y
+     od	
+  fi
+od

benchmarks/temporal/gc/nd_af_ag_emp.ctl

@@ -0,0 +1,18 @@
+fields: next;
+precondition:ls(x,nil);
+property: AF(AG(emp));
+while x=x do
+    if * then
+        while x!=nil do
+            temp:=x.next;
+            free(x);
+            x:=temp
+        od
+    else
+        while * do
+	    y:=new();
+	    y.next:=x;
+	    x:=y
+	od
+    fi
+od

benchmarks/temporal/gc/nd_af_eg_emp.ctl

@@ -1,6 +1,6 @@
 fields: next;
 precondition:ls(x,nil);
-property: AG(EG(ls(x,nil)));
+property: AF(EG(emp));
 while x=x do
     if * then
         while x!=nil do

benchmarks/temporal/gc/nd_af_emp.ctl

@@ -0,0 +1,18 @@
+fields: next;
+precondition:x!=nil * ls(x,nil);
+property: AF(emp);
+while x=x do
+    if * then
+        while x!=nil do
+            temp:=x.next;
+            free(x);
+            x:=temp
+        od
+    else
+        while * do
+	    y:=new();
+	    y.next:=x;
+	    x:=y
+	od
+    fi
+od

benchmarks/temporal/gc/nd_ag_af_emp.ctl

@@ -0,0 +1,18 @@
+fields: next;
+precondition:ls(x,nil);
+property: AG(AF(emp));
+while x=x do
+    if * then
+        while x!=nil do
+            temp:=x.next;
+            free(x);
+            x:=temp
+        od
+    else
+        while * do
+	    y:=new();
+	    y.next:=x;
+	    x:=y
+	od
+    fi
+od

benchmarks/temporal/gc/nd_ag_eg_ls.ctl

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

benchmarks/temporal/microbench/afagp_s.ctl

@@ -1,5 +1,5 @@
 fields: next;
-precondition: current=zero * x=zero * zero->one * one->two * two->three * three->four * four->five * FALSE->false' * TRUE->true' * break=FALSE;
+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

benchmarks/temporal/microbench/afef_s.ctl

@@ -1,5 +1,5 @@
 fields: next;
-precondition: current=zero * x=zero * zero->one * one->two * two->three * three->four * four->five * FALSE->false' * TRUE->true' * break=FALSE;
+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
@@ -9,7 +9,7 @@ while break=FALSE do
   fi
 od;
 break:=FALSE;
-current:=zero;
+current:=four;
 while break=FALSE do
   if current=five then
     break:=TRUE

benchmarks/temporal/microbench/afp_s.ctl

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

benchmarks/temporal/microbench/afp_s_old.ctl

@@ -0,0 +1,14 @@
+fields: next;
+precondition: n->one * one->zero * zero->nil * p=zero * current=n * FALSE->false' * TRUE->true';
+property: AF(p=one);
+while break=FALSE do
+  if current=zero then
+    break:=TRUE
+  else
+    current:=current.next
+  fi
+od;
+p:=one;
+while TRUE=TRUE do
+  skip
+od

benchmarks/temporal/microbench/agafp_s.ctl

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

benchmarks/temporal/microbench/agafp_s_old.ctl

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

benchmarks/temporal/microbench/agef_s_heap.ctl

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

benchmarks/temporal/microbench/ageg_s_heap_nd.ctl

@@ -0,0 +1,13 @@
+fields: left,right;
+precondition: x!=nil * bt(x);
+property: AG(AF(x!=nil));
+while x=x do
+  if * then
+    temp:=new();
+    temp.left:=x;
+    temp.right:=nil;
+    x:=temp
+  else
+    x:=nil
+  fi
+od

benchmarks/temporal/microbench/agimpef_s.ctl

@@ -1,5 +1,5 @@
 fields: next;
-precondition: current=zero * check=zero * p=zero * zero->one * one->two * two->three * three->four * four->five * FALSE->false' * TRUE->true' * break=FALSE;
+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