Merge pull request #18 from isaacmaffeis/isaac

Isaac

asmetal2java_codegen/examples/ATM3.asm

@@ -230,4 +230,4 @@ default init s0:
 										case card2 : 1652
 										case card3 : 548
 									endswitch
-	function accessible($c in NumCard) = true	
+	function accessible($c in NumCard) = true

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:

asmetal2java_codegen/src/org/asmeta/asm2java/RuleToJava.xtend

@@ -166,10 +166,15 @@ class RuleToJava extends RuleVisitor<String> {
 				append('''«new TermToJava(res,true).visit(object.location)» = «new TermToJava(res,false).visit(object.updatingTerm)»;
 			   
 			''')
-		else if (object.updatingTerm.domain instanceof ConcreteDomain)
+		/*else if (object.updatingTerm.domain instanceof ConcreteDomain)
 			result.
 				append('''«new TermToJava(res,true).visit(object.location)»«new TermToJava(res,false).visit(object.updatingTerm)».value);
 			   «new TermToJavaInUpdateRule(res,false).visit(object.location)»
+			''')*/
+		else if (object.updatingTerm.domain instanceof ConcreteDomain)
+			result.
+				append('''«new TermToJava(res,true).visit(object.location)»«new TermToJava(res,false).visit(object.updatingTerm)»);
+			   «new TermToJavaInUpdateRule(res,false).visit(object.location)»
 			''')
 		else {
 			var String varName = object.hashCode.toString

asmetal2java_codegen/src/org/asmeta/asm2java/TermToJava.xtend

@@ -233,6 +233,11 @@ class TermToJava extends ReflectiveVisitor<String> {
 			'''
 					«"Arrays.stream("»	«new ToString(res).visit((object.getRanges.get(i).domain as PowersetDomain).baseDomain)».values()).anyMatch(c -> «valore»c))
 				''')
+			else if ((object.getRanges.get(i).domain as PowersetDomain).baseDomain instanceof ConcreteDomain) // devo togliere il .value aggiunto in TermToJavaStandardLibrary.xtend (riga 102)  
+				sb.append(
+			'''
+					«""»	«new ToString(res).visit((object.getRanges.get(i).domain as PowersetDomain).baseDomain)».elems.stream().anyMatch(c -> c.equals(«app.substring(13,app.length-7)»))
+				''')
 			else
 				sb.append(
 			'''
@@ -371,9 +376,13 @@ class TermToJava extends ReflectiveVisitor<String> {
 		var name = new Util().parseFunction(term.function.name)
 
 		// Controllo se l'operatore » del tipo: &,|,<=,>=,<,>...
-		if (ExpressionToJava.hasEvaluateVisitor(name)) {
+		/*if (ExpressionToJava.hasEvaluateVisitor(name)) {
+			// if the funcion is an expression
+			return new ExpressionToJava(res).evaluateFunction(name, term.arguments.terms);*/
+		if (ExpressionToJava.hasEvaluateVisitor(name)) { // utilizzo questo if per correggere il problema di avere due .value.value
 			// if the funcion is an expression
-			return new ExpressionToJava(res).evaluateFunction(name, term.arguments.terms);
+			var expression = new ExpressionToJava(res).evaluateFunction(name, term.arguments.terms);
+			return expression.replaceAll(".value.value",".value")
 		} // In questo caso l'operatore rilevato » := 
 		else {