add abstract domain support

Author: isaacmaffeis

asmetal2java_codegen/input/CTLLibrary.asm

@@ -0,0 +1,65 @@
+module CTLLibrary
+
+import StandardLibrary
+
+export *
+
+signature:
+	/*-----------CTL formulas------------*/
+	static eg: Boolean -> Boolean	//exists globally
+	static ex: Boolean -> Boolean	//exists next state
+	static ef: Boolean -> Boolean	//exists finally
+	static ag: Boolean -> Boolean	//forall globally
+	static ax: Boolean -> Boolean	//forall next state
+	static af: Boolean -> Boolean	//forall finally
+	static eu: Prod(Boolean, Boolean) -> Boolean	//exists until
+	static au: Prod(Boolean, Boolean) -> Boolean //forall until
+
+	/*-----------Patterns------------*/
+	static ew: Prod(Boolean, Boolean) -> Boolean  //exists weak until -- E[p U q] | EGp.
+	static aw: Prod(Boolean, Boolean) -> Boolean //forall weak until -- !E[!q U !(p | q)].
+
+
+	//http://patterns.projects.cis.ksu.edu/documentation/patterns/ctl.shtml
+	//Absence (P is false)
+	//Globally - AG(!P)
+	static absenceG: Boolean -> Boolean
+	//(*) Before R - A[(!P | AG(!R)) W R]
+	static absenceBefore: Prod(Boolean, Boolean) -> Boolean // absenceBefore(P, R)
+	//After Q - AG(Q -> AG(!P))
+	static absenceAfter: Prod(Boolean, Boolean) -> Boolean // absenceAfter(P, Q)
+	//(*) Between Q and R - AG(Q & !R -> A[(!P | AG(!R)) W R])
+	static absenceBetween: Prod(Boolean, Boolean, Boolean) -> Boolean // absenceBetween(P, Q, R)
+	//(*) After Q until R - AG(Q & !R -> A[!P W R])
+	static absenceAfterUntil: Prod(Boolean, Boolean, Boolean) -> Boolean // absenceAfterUntil(P, Q, R)
+
+	//Precedence (S precedes P)
+	//(*) Globally 	
+	//A[!P W S]
+	static ap: Prod(Boolean, Boolean) -> Boolean // ap(P, S)
+	//(*) Before R 	
+	//A[(!P | AG(!R)) W (S | R)]
+	static pb: Prod(Boolean, Boolean, Boolean) -> Boolean // pb(P, S, R)
+	//(*) After Q 	
+	//A[!Q W (Q & A[!P W S])]
+	//(*) Between Q and R 	
+	//AG(Q & !R -> A[(!P | AG(!R)) W (S | R)])
+	//(*) After Q until R 	
+	//AG(Q & !R -> A[!P W (S | R)])
+
+	//Response (S responds to P)
+	//Globally
+	//AG(P -> AF(S))
+	//(*) Before R	
+	//A[((P -> A[!R U (S & !R)]) | AG(!R)) W R]
+	//(*) After Q	
+	//A[!Q W (Q & AG(P -> AF(S))] 
+	//(*) Between Q and R	
+	//AG(Q & !R -> A[((P -> A[!R U (S & !R)]) | AG(!R)) W R])
+	//(*) After Q until R	
+	//AG(Q & !R -> A[(P -> A[!R U (S & !R)]) W R])
+
+	/*-----------My CTL formulas------------*/
+	static exN: Prod(Boolean, Natural) -> Boolean	//exists after N states
+	static axN: Prod(Boolean, Natural) -> Boolean	//forall paths, after N states
+definitions:

asmetal2java_codegen/input/LTLLibrary.asm

@@ -0,0 +1,21 @@
+module LTLLibrary
+
+export *
+
+signature:
+	/*-----------LTL formulas------------*/ 
+	//Future
+	static x: Boolean -> Boolean			//next state
+	static g: Boolean -> Boolean			//globally
+	static f: Boolean -> Boolean			//finally
+	static u: Prod(Boolean, Boolean) -> Boolean	//until
+	static v: Prod(Boolean, Boolean) -> Boolean	//releases
+	//Past
+	static y: Boolean -> Boolean			//previous state
+	static z: Boolean -> Boolean			//not previous state not
+	static h: Boolean -> Boolean			//historically
+	static o: Boolean -> Boolean			//once
+	static s: Prod(Boolean, Boolean) -> Boolean	//since
+	static t: Prod(Boolean, Boolean) -> Boolean	//triggered
+
+definitions: