Changes to fix bug #303

core/analysis/modelchecker/src/main/java/eu/compassresearch/core/analysis/modelchecker/ast/actions/MCACommunicationAction.java

@@ -108,9 +108,11 @@ public String toFormula(String option) {
 		valuesCopy.addAll(values);
 
 		if(chanDef.isInfiniteType()){
-			String infiniteVarName = this.communicationParameters.getFirst().toString();
-			context.variablesInfiniteDomain.add(infiniteVarName);
-			result.append(buildPrefix(option, context, true));
+
+			if(!parameterIsConstantValue()){
+				String infiniteVarName = this.communicationParameters.getFirst().toString();
+				context.variablesInfiniteDomain.add(infiniteVarName);
+				result.append(buildPrefix(option, context, true));
 			/*
 			if(!parameterIsConstantValue()){
 				String actionNameToUse = ""; 
@@ -129,6 +131,9 @@ public String toFormula(String option) {
 			}
 			*/
 			context.variablesInfiniteDomain.remove(infiniteVarName);
+			} else{
+				result.append(buildPrefix(option, context, true));
+			}
 		} else{
 			//int i = 0;
 			//result.append(buildReplicatedExternalChoice(context, values, option, allParamsCopy,false));
@@ -309,6 +314,7 @@ public String buildIOCommActualParams(String option){
 		ExpressionEvaluator evaluator = ExpressionEvaluator.getInstance();
 
 		if(option.equals(MCNode.MINIMAL_GENERIC) || option.equals(MCNode.STATE_DEFAULT_PROCESS_NAMED)){
+
 			MCPCMLType type = evaluator.instantiateMCTypeFromCommParamsForIOCommDef(this.communicationParameters,"");
 			result.append(type.toFormula(option));
 		}else{

core/analysis/modelchecker/src/main/java/eu/compassresearch/core/analysis/modelchecker/ast/auxiliary/ExpressionEvaluator.java

@@ -76,6 +76,8 @@ public MCPCMLType getTypeFor(MCPCMLExp exp){
 			result = this.getTypeFor((MCABooleanConstExp)exp);
 		} else if(exp instanceof MCAInSetBinaryExp){
 			result = this.getTypeFor((MCAInSetBinaryExp)exp);
+		} else if(exp instanceof MCAUnaryMinusUnaryExp){
+			result = this.getTypeFor((MCAUnaryMinusUnaryExp)exp);
 		}
 
 		return result;
@@ -85,6 +87,8 @@ private MCPCMLType getTypeForIOComm(MCPCMLExp exp){
 		MCPCMLType result = null;
 		if(exp instanceof MCAIntLiteralExp){
 			result = this.getTypeFor((MCAIntLiteralExp)exp);
+		} else if(exp instanceof MCAUnaryMinusUnaryExp){
+			result = this.getTypeFor((MCAUnaryMinusUnaryExp)exp);
 		} else if(exp instanceof MCARealLiteralExp){
 			result = this.getTypeFor((MCARealLiteralExp)exp);
 		} else if(exp instanceof MCAVariableExp){
@@ -172,6 +176,7 @@ public MCPCMLType getTypeFor(MCPCommunicationParameter param){
 
 	public MCPCMLType getTypeForIOComm(MCPCommunicationParameter param){
 		MCPCMLType result = null;
+
 		if(param instanceof MCASignalCommunicationParameter){
 			result = this.getTypeForIOComm((MCASignalCommunicationParameter)param);
 		} else if(param instanceof MCAReadCommunicationParameter){
@@ -280,7 +285,6 @@ public MCPCMLType instantiateMCTypeFromParams(LinkedList<MCPParametrisation> par
 
 		return result;
 	}
-
 	public MCPCMLType instantiateMCTypeFromCommParams(LinkedList<MCPCommunicationParameter> params){
 		MCPCMLType result = null;
 
@@ -405,6 +409,13 @@ private MCPCMLType getTypeFor(MCAIntLiteralExp exp){
 
 		return result;
 	}
+	private MCPCMLType getTypeFor(MCAUnaryMinusUnaryExp exp){
+		MCPCMLType result = null;
+
+		result = new MCAIntNumericBasicType("-" + exp.getExp().toFormula(MCNode.DEFAULT));
+
+		return result;
+	}
 	private MCPCMLType getTypeFor(MCARealLiteralExp exp){
 		MCPCMLType result = null;
 

core/analysis/modelchecker/src/main/java/eu/compassresearch/core/analysis/modelchecker/ast/expressions/MCAUnaryMinusUnaryExp.java

@@ -2,6 +2,7 @@
 
 import java.util.LinkedList;
 
+import eu.compassresearch.core.analysis.modelchecker.ast.MCNode;
 import eu.compassresearch.core.analysis.modelchecker.ast.auxiliary.PatternValue;
 
 public class MCAUnaryMinusUnaryExp implements MCPCMLExp {
@@ -19,6 +20,12 @@ public String toFormula(String option) {
 		return "-" + this.exp.toFormula(option);
 	}
 
+
+	@Override
+	public String toString() {
+		return toFormula(MCNode.DEFAULT);
+	}
+
 	@Override
 	public MCPCMLExp copy() {
 

core/analysis/modelchecker/src/main/java/eu/compassresearch/core/analysis/modelchecker/visitors/NewMCVisitor.java

@@ -365,7 +365,7 @@ public static void main(String[] args) throws Throwable {
 		//String cml_file = "src/test/resources/action-condchoice.cml";
 		//String cml_file = "src/test/resources/Param.cml";
 		//String cml_file = "src/test/resources/inf.cml";
-		String cml_file = "src/test/resources/T243v2-MC.cml";
+		String cml_file = "src/test/resources/BorderTrafficMC_v1.cml";
 
 
 
@@ -378,11 +378,12 @@ public static void main(String[] args) throws Throwable {
 		//String cml_file = "src/test/resources/simpler-insielImpl-final-modelchecker.cml";
 		//String cml_file = "src/test/resources/action-prefix-skip.cml";
 		//System.out.println("Testing on " + cml_file);
-		PSource source1 = Utilities.makeSourceFromFile(cml_file);
+		PSource ast = Utilities.makeSourceFromFile(cml_file);
 		// Type check
 		ITypeIssueHandler errors = VanillaFactory.newCollectingIssueHandle();
-		ICmlTypeChecker cmlTC = VanillaFactory.newTypeChecker(source1.getParagraphs(), errors);
-
+		ICmlTypeChecker cmlTC = VanillaFactory.newTypeChecker(
+				ast.getParagraphs(), errors);
+
 		/*
 		if(!cmlTC.typeCheck()){
 			System.out.println("There are typecheck errors.");
@@ -392,7 +393,7 @@ public static void main(String[] args) throws Throwable {
 		//String mainProcessName = "Test_TurnOnProduct";
 				//String mainProcessName = "TargetProduct_DD_SD_InterfaceProtocolView";
 
-		String mainProcessName = "Renderers";
+		String mainProcessName = "CountryTMS";
 				//String mainProcessName = "RegisterProc";
 				//String mainProcessName = "N_LAZY_Q";
 				//String mainProcessName = "StreamingPlayerCSProcess";
@@ -418,7 +419,7 @@ public static void main(String[] args) throws Throwable {
 		NewMCVisitor visitor1 = new NewMCVisitor();
 
 
-		String formulaCode = visitor1.generateFormulaScript(source1.getParagraphs(),Utilities.DEADLOCK_PROPERTY,mainProcessName);
+		String formulaCode = visitor1.generateFormulaScript(ast.getParagraphs(),Utilities.DEADLOCK_PROPERTY,mainProcessName);
 		//String[] codes1 = visitor1.generateFormulaCodeForAll(Utilities.DEADLOCK_PROPERTY);
 		//for (int j = 0; j < codes1.length; j++) {
 		//	System.out.println(codes1[j]);

core/analysis/modelchecker/src/main/java/eu/compassresearch/core/analysis/modelchecker/visitors/Utilities.java

@@ -21,9 +21,6 @@
 import eu.compassresearch.ast.program.AFileSource;
 import eu.compassresearch.ast.program.AInputStreamSource;
 import eu.compassresearch.ast.program.PSource;
-import eu.compassresearch.core.analysis.modelchecker.graphBuilder.type.Int;
-import eu.compassresearch.core.analysis.modelchecker.graphBuilder.type.Type;
-import eu.compassresearch.core.analysis.modelchecker.graphBuilder.type.Void;
 import eu.compassresearch.core.parser.CmlLexer;
 import eu.compassresearch.core.parser.CmlParser;
 
@@ -65,13 +62,15 @@ public class Utilities {
 	private static boolean parseWithANTLR(PSource sourceIn) throws IOException
 	{
 		ANTLRInputStream in = null;
-		
+
 		if (sourceIn instanceof AInputStreamSource)
-			in = new ANTLRInputStream(((AInputStreamSource)sourceIn).getStream());
-
+			in = new ANTLRInputStream(
+					((AInputStreamSource) sourceIn).getStream());
+
 		if (sourceIn instanceof AFileSource)
-			in = new ANTLRInputStream( new FileInputStream(((AFileSource)sourceIn).getFile()));
-
+			in = new ANTLRInputStream(new FileInputStream(
+					((AFileSource) sourceIn).getFile()));
+
 		CmlLexer lexer = new CmlLexer(in);
 		CommonTokenStream tokens = new CommonTokenStream(lexer);
 		CmlParser parser = new CmlParser(tokens);
@@ -80,25 +79,11 @@ private static boolean parseWithANTLR(PSource sourceIn) throws IOException
 			sourceIn.setParagraphs(parser.source());
 			return true;
 		} catch (RecognitionException e) {
-			e.printStackTrace();
 			return false;
 		}
 
 	}
 
-	public static Type createValue(PExp expression){
-		Type result = null;
-
-		if(expression == null){
-			result = new Void();
-		}
-		if(expression instanceof AIntLiteralExp){
-			result = new Int(Integer.valueOf(((AIntLiteralExp) expression).getValue().toString()));
-		}
-
-		return result;
-	}
-
 	public static String extractFunctionName(String functionCall){
 		String result = functionCall;
 		int index = functionCall.indexOf("(");

core/analysis/modelchecker/src/test/resources/BorderTrafficMC_v1.cml

@@ -0,0 +1,145 @@
+types
+
+  CountryId = nat
+  ActuatorId =nat
+
+  Location = int
+
+functions
+
+   -- Function to calculate the distance required for the corridor based upon the target
+   -- speed and the current national speed limit of the country.
+   calcDistance: nat * nat -> nat
+   calcDistance(targetSpeed, speedLimit) == ((speedLimit-targetSpeed)/maxInterval) + 1  -- simplified for MC
+
+   -- Function to calculate the speed target the neighbouring TMS must acheive. THis is based 
+   -- upon the starting location of the corridor, the required distance of the corridor, and the
+   -- ultimate target speed
+   calcNeighbourTarget : int * nat * nat * nat -> nat   
+   calcNeighbourTarget(startLoc, target, distance, speedLimit)  ==
+      target + (calcInterval(target, distance, speedLimit) * startLoc)
+
+
+  calcInterval: nat * nat * nat -> nat
+  calcInterval(target, distance, speedLimit) == ((speedLimit-target)/distance)
+   pre speedLimit > target and distance > 0   
+
+
+   --Determines if Neighbour is needed based upon the starting location and distance of the
+   -- speed corridor
+   --**IMPORTANT** current model of location means this is only valid for Country B!
+   isNeighbourNeeded : int * nat -> bool
+   isNeighbourNeeded (startLoc, distance) == startLoc + distance > 0
+
+channels
+
+  --environment channels--
+  inIncidentOne : CountryId
+  inIncidentTwo : Location
+  inIncidentThree : nat
+  incidentClearOne: CountryId 
+  incidentClearTwo: Location
+
+  --interface channels--
+  neighbourRequestOne : CountryId
+  neighbourRequestTwo :  CountryId
+  neighbourRequestThree : nat
+  neighbourOkOne : CountryId
+  neighbourOkTwo : CountryId
+
+
+  --internal corridor channels--
+  determineCorrOne : int 
+  determineCorrTwo : nat
+  newCorr 
+  createCorr
+  disableCorr
+
+
+chansets
+  -- the main interface between countryTMSs
+  interface = {neighbourRequestOne, neighbourRequestTwo, neighbourRequestThree, neighbourOkOne, neighbourOkTwo}
+
+  -- interface of SoS and incident creator
+  incident = {inIncidentOne, inIncidentTwo, inIncidentThree, incidentClearOne, incidentClearTwo}
+
+  --internal channels--
+  internal = {determineCorrOne, determineCorrTwo, newCorr, createCorr, disableCorr}
+
+
+process CountryTMS =  i:CountryId, n:CountryId, sl:nat@
+begin
+
+ state
+  -- identifiers for the TMS and its neighbour
+  myId : CountryId := i
+  nId : CountryId :=n
+  nationalSpeedLimit : nat :=sl
+
+ actions
+
+   BEHAVIOUR = NEW_INCIDENT [] NEIGHBOUR_REQ
+
+   NEW_INCIDENT = inIncidentOne.myId -> inIncidentTwo?l -> inIncidentThree?t -> 
+                  (dcl d : nat := calcDistance(t, nationalSpeedLimit) @ 
+                   NEW_CORRIDOR(l, t, d))
+
+   NEW_CORRIDOR = l : int, t: nat, d:nat @ 
+                 (newCorr -> Skip; 
+     			  (dcl neighbourNeeded : bool := isNeighbourNeeded(l, d) @
+                   ([neighbourNeeded]     & (dcl ntarg:nat := calcNeighbourTarget(l, t, d, nationalSpeedLimit) @
+                                              neighbourRequestOne!myId -> neighbourRequestTwo!nId -> 
+                                              neighbourRequestThree!ntarg -> CLEAR_INCIDENT(l,true))
+                    []
+                    [not neighbourNeeded] & CLEAR_INCIDENT(l, false))))
+
+   CLEAR_INCIDENT = l:int, neigh:bool @ 
+  			   (incidentClearOne.myId -> incidentClearTwo.l ->  CLEAR_CORRIDOR(neigh))
+
+   CLEAR_CORRIDOR = neigh:bool @ 
+                     [neigh]& disableCorr -> Skip; neighbourOkOne!myId -> neighbourOkTwo!nId -> NEW_INCIDENT
+                     []
+                     [not neigh] & disableCorr -> Skip; BEHAVIOUR 
+
+   NEIGHBOUR_REQ = neighbourRequestOne.nId -> neighbourRequestTwo.myId -> neighbourRequestThree?t -> newCorr -> Skip; NEIGHBOUR_CLEAR
+
+   NEIGHBOUR_CLEAR =  neighbourOkOne.nId -> neighbourOkTwo.myId -> disableCorr -> Skip; BEHAVIOUR
+
+
+  @ BEHAVIOUR			
+end 
+
+process CountryA = CountryTMS(theAId, theBId, limitA)
+process CountryB = CountryTMS(theBId, theAId, limitB)
+
+process BorderTrafficSoS = CountryA [|interface|] CountryB --\\ internal
+
+
+process Scenario = 
+begin 
+  @ inIncidentOne!theBId -> inIncidentTwo!(-4) -> inIncidentThree!20 -> 
+    incidentClearOne.theBId -> incidentClearTwo.(-4)-> 
+    inIncidentOne.theBId -> inIncidentTwo.(-1) -> inIncidentThree.20 -> 
+    incidentClearOne.theBId -> incidentClearTwo.(-1) -> Skip 
+end
+
+process Test = Scenario [|incident|] BorderTrafficSoS
+
+
+-- Values are used in the scenarios
+values
+
+  maxDiff : nat = 20
+  maxChange : nat = 40
+
+  theAId : CountryId = 1
+  theBId :CountryId = 2
+
+  limitA : nat = 100
+  limitB : nat = 90
+
+
+  restrictionSpeed : nat = 20
+  blockageSpeed : nat = 5
+
+  maxInterval : nat = 40