Simple Vacuity Checking Added

.gitignore

@@ -58,3 +58,4 @@ pes.timed/test/dbmtest[1]_include.cmake
 pes.timed/test/parsetest[1]_include.cmake
 pes.timed/test/prooftest[1]_include.cmake
 Doxyfile.doxygen
+.DS_Store

README.md

@@ -89,7 +89,17 @@ The executable program is named `timesolver-ta`.
 
 To run, use `timesolver-ta <exampleFile>`
 
-Example files are included in the `example` directory 
+Example files are included in the `example` directory.
+
+### Program Outputs
+
+The program will output whetehr the formula is vaild or invalid, with the running time. Furthermore, a simple
+vacuity is implemented. This program will also identify any unchecked subformulas. This provides a sound
+but incomplete vacuity checking for the formula. We know that any subformula not examined during the proof does not 
+affect the truth of the formula (soundness), however it may check subformula it does not need to check (incompleteness).
+The prover checks subformula from left to right.
+
+To see the entire proof, enable the `-d` option.
 
 ## Generating Examples
 

examples/AdditionalVacuityCases/PFThesisFig6-1aF1.in

@@ -0,0 +1,13 @@
+CLOCKS :{x1, x2}
+CONTROL :{p1(2)}
+PREDICATE: {X1, X2}
+START: X1
+EQUATIONS: {
+1: nu X1 = (p1 != 1 || X2) && (\forall time(X1 && \AllAct(X1)))
+2: mu X2 = (p1 == 1) || (\forall time(X2 && \AllAct(X2)))
+	}
+INVARIANT:
+	p1 == 1 -> x1 <= 50
+TRANSITIONS:
+	(p1==0, x2 >= 2)->(p1=1){x2};
+	(p1==1)->(p1=0){x2};

examples/AdditionalVacuityCases/PFThesisFig6-1bF1.in

@@ -0,0 +1,13 @@
+CLOCKS :{x1, x2}
+CONTROL :{p1(2)}
+PREDICATE: {X1, X2}
+START: X1
+EQUATIONS: {
+1: nu X1 = (p1 != 1 || X2) && (\forall time(X1 && \AllAct(X1)))
+2: mu X2 = (p1 == 1) || (\forall time(X2 && \AllAct(X2)))
+	}
+INVARIANT:
+	p1 == 0 -> x1 >= 0
+TRANSITIONS:
+	(p1==0)->(p1=0){x1};
+	(p1==1)->(p1=0){x2};

examples/AdditionalVacuityCases/PFThesisFig6-2F1.in

@@ -0,0 +1,18 @@
+CLOCKS :{x1}
+CONTROL :{p1(5), p(2), q(2)}
+PREDICATE: {X1, X2, X3}
+START: X1
+EQUATIONS: {
+1: nu X1 = \AllAct(X2 || X3)
+2: mu X2 = (p == 1) || (\forall time(X2 && \AllAct(X2)))
+3: mu X3 = (q == 1) || (\forall time(X3 && \AllAct(X3)))
+	}
+INVARIANT:
+  	p1 == 0 -> x1 >= 0
+TRANSITIONS:
+	(p1==0)->(p1=1, p=1, q=0);
+  (p1==0)->(p1=2, q=1, p=0);
+	(p1==1)->(p1=3, q=1, p=0);
+  (p1==3)->(p1=3, q=1, p=0);
+  (p1==2)->(p1=4, p=1, q=0);
+  (p1==4)->(p1=4, p=1, q=0);

examples/AdditionalVacuityCases/PFThesisFig6-2F1s.in

@@ -0,0 +1,18 @@
+CLOCKS :{x1}
+CONTROL :{p1(5), p(2), q(2)}
+PREDICATE: {X1, X2, X3}
+START: X1
+EQUATIONS: {
+1: nu X1 = \AllAct(X2 |s| X3)
+2: mu X2 = (p == 1) |s| \AllAct(X2)
+3: mu X3 = (q == 1) |s| \AllAct(X3)
+	}
+INVARIANT:
+  	p1 == 0 -> x1 >= 0
+TRANSITIONS:
+	(p1==0)->(p1=1, p=1, q=0);
+  (p1==0)->(p1=2, q=1, p=0);
+	(p1==1)->(p1=3, q=1, p=0);
+  (p1==3)->(p1=3, q=1, p=0);
+  (p1==2)->(p1=4, p=1, q=0);
+  (p1==4)->(p1=4, p=1, q=0);

examples/AdditionalVacuityCases/PFThesisFig6-2F1sb.in

@@ -0,0 +1,17 @@
+CLOCKS :{x1}
+CONTROL :{p1(5), p(2), q(2)}
+PREDICATE: {X1, X2, X3}
+START: X1
+EQUATIONS: {
+1: nu X1 = \AllAct(X2)
+2: mu X2 = (p == 1) |s| \AllAct(X2)
+	}
+INVARIANT:
+  	p1 == 0 -> x1 >= 0
+TRANSITIONS:
+	(p1==0)->(p1=1, p=1, q=0);
+  (p1==0)->(p1=2, q=1, p=0);
+	(p1==1)->(p1=3, q=1, p=0);
+  (p1==3)->(p1=3, q=1, p=0);
+  (p1==2)->(p1=4, p=1, q=0);
+  (p1==4)->(p1=4, p=1, q=0);