diff --git a/core/analysis/modelchecker/src/main/java/eu/compassresearch/core/analysis/modelchecker/ast/actions/MCACommunicationAction.java b/core/analysis/modelchecker/src/main/java/eu/compassresearch/core/analysis/modelchecker/ast/actions/MCACommunicationAction.java index 2c284eda7..58d9dd993 100644 --- a/core/analysis/modelchecker/src/main/java/eu/compassresearch/core/analysis/modelchecker/ast/actions/MCACommunicationAction.java +++ b/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{ diff --git a/core/analysis/modelchecker/src/main/java/eu/compassresearch/core/analysis/modelchecker/ast/auxiliary/ExpressionEvaluator.java b/core/analysis/modelchecker/src/main/java/eu/compassresearch/core/analysis/modelchecker/ast/auxiliary/ExpressionEvaluator.java index f7bae9af5..8e9c18804 100644 --- a/core/analysis/modelchecker/src/main/java/eu/compassresearch/core/analysis/modelchecker/ast/auxiliary/ExpressionEvaluator.java +++ b/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 par return result; } - public MCPCMLType instantiateMCTypeFromCommParams(LinkedList 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; diff --git a/core/analysis/modelchecker/src/main/java/eu/compassresearch/core/analysis/modelchecker/ast/expressions/MCAUnaryMinusUnaryExp.java b/core/analysis/modelchecker/src/main/java/eu/compassresearch/core/analysis/modelchecker/ast/expressions/MCAUnaryMinusUnaryExp.java index a6ebf4f07..b993d6d79 100644 --- a/core/analysis/modelchecker/src/main/java/eu/compassresearch/core/analysis/modelchecker/ast/expressions/MCAUnaryMinusUnaryExp.java +++ b/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() { diff --git a/core/analysis/modelchecker/src/main/java/eu/compassresearch/core/analysis/modelchecker/visitors/NewMCVisitor.java b/core/analysis/modelchecker/src/main/java/eu/compassresearch/core/analysis/modelchecker/visitors/NewMCVisitor.java index 8b6d6423a..7d810ea84 100644 --- a/core/analysis/modelchecker/src/main/java/eu/compassresearch/core/analysis/modelchecker/visitors/NewMCVisitor.java +++ b/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]); diff --git a/core/analysis/modelchecker/src/main/java/eu/compassresearch/core/analysis/modelchecker/visitors/Utilities.java b/core/analysis/modelchecker/src/main/java/eu/compassresearch/core/analysis/modelchecker/visitors/Utilities.java index 27789176c..b005f193b 100644 --- a/core/analysis/modelchecker/src/main/java/eu/compassresearch/core/analysis/modelchecker/visitors/Utilities.java +++ b/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("("); diff --git a/core/analysis/modelchecker/src/test/resources/BorderTrafficMC_v1.cml b/core/analysis/modelchecker/src/test/resources/BorderTrafficMC_v1.cml new file mode 100644 index 000000000..794e1926a --- /dev/null +++ b/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 diff --git a/ide/plugins/modelchecker/src/main/java/eu/compassresearch/ide/modelchecker/MCUnsupportedCollector.java b/ide/plugins/modelchecker/src/main/java/eu/compassresearch/ide/modelchecker/MCUnsupportedCollector.java index 631bd1a95..f7d0e9947 100644 --- a/ide/plugins/modelchecker/src/main/java/eu/compassresearch/ide/modelchecker/MCUnsupportedCollector.java +++ b/ide/plugins/modelchecker/src/main/java/eu/compassresearch/ide/modelchecker/MCUnsupportedCollector.java @@ -1,6 +1,8 @@ package eu.compassresearch.ide.modelchecker; +import java.util.ArrayList; import java.util.LinkedList; +import java.util.List; import org.overture.ast.analysis.AnalysisException; import org.overture.ast.definitions.AAssignmentDefinition; @@ -193,6 +195,7 @@ import eu.compassresearch.ast.actions.AVresParametrisation; import eu.compassresearch.ast.actions.AWaitAction; import eu.compassresearch.ast.actions.AWriteCommunicationParameter; +import eu.compassresearch.ast.actions.PParametrisation; import eu.compassresearch.ast.declarations.AExpressionSingleDeclaration; import eu.compassresearch.ast.declarations.ATypeSingleDeclaration; import eu.compassresearch.ast.definitions.AActionClassDefinition; @@ -595,14 +598,14 @@ public void caseAChannelRenamingProcess(AChannelRenamingProcess node) } @Override - public void caseAChannelType(AChannelType arg0) throws AnalysisException { + public void caseAChannelType(AChannelType node) throws AnalysisException { //channel types that have more than one communication type are not allowed UnsupportedElementInfo uei = new UnsupportedElementInfo() { }; - if(arg0.getParameters().size() > 1){ - uei.setLocation(arg0.getLocation()); - uei.setMessage(arg0.getClass().getSimpleName().toString() + if(node.getParameters().size() > 1){ + uei.setLocation(node.getLocation()); + uei.setMessage(node.getClass().getSimpleName().toString() + " nodes with more than one parameter are not supported by the " + this.getFeature().toString()); this.getUnsupporteds().add(uei); unsupported = true; @@ -2319,9 +2322,41 @@ public void caseAPrivateAccess(APrivateAccess node) @Override public void caseAProcessDefinition(AProcessDefinition node) throws AnalysisException { - unsupported = false; + //unsupported = false; + UnsupportedElementInfo uei = new UnsupportedElementInfo() { + }; + + if(node.getLocalState().size() > 1){ + uei.setLocation(node.getName().getLocation()); + uei.setMessage(node.getClass().getSimpleName().toString() + + " nodes with more than one parameter are not supported by the " + this.getFeature().toString()); + this.getUnsupporteds().add(uei); + unsupported = true; + }else{ + unsupported = false; + } // Do not remove the super call below. - super.caseAProcessDefinition(node); + //super.caseAProcessDefinition(node); + //the super class call above inserts two UnsupportedElementInfo in the list. We changed it with the code bellow + //to avoid that. + if(node.getClassDefinition() != null && !_visitedNodes.contains(node.getClassDefinition())) { + node.getClassDefinition().apply(this); + } + { + List copy = new ArrayList(node.getLocalState()); + for( PParametrisation e : copy) + { + if(!_visitedNodes.contains(e)) + { + e.apply(this); + } + } + } + if(node.getProcess() != null && !_visitedNodes.contains(node.getProcess())) + { + node.getProcess().apply(this); + } + } @Override