Merge branch 'development'

Author: joey-coleman

README.md

@@ -0,0 +1,10 @@
+symphony
+========
+
+The Symphony IDE is a tool being developed as part of the COMPASS EU FP7 research project. 
+
+> The COMPASS consortium is a group of researchers and companies committed to collaborative research on model-based techniques for developing and maintaining Systems of Systems (SoS).
+
+-- From the COMPASS website: http://www.compass-research.eu/
+
+Symphony is developed as an extension to Overture, which you can check out at http://overturetool.org/

…r/src/test/resources/beo-spec-simple.cml …nalysis/modelchecker/beo-spec-simple.cmlcore/analysis/modelchecker/src/test/resources/beo-spec-simple.cml renamed to core/analysis/modelchecker/beo-spec-simple.cml core/analysis/modelchecker/src/test/resources/beo-spec-simple.cml renamed to core/analysis/modelchecker/beo-spec-simple.cml

@@ -5,7 +5,7 @@
   <parent>
     <groupId>eu.compassresearch.core.analysis</groupId>
     <artifactId>analysis</artifactId>
-    <version>0.3.2</version>
+    <version>0.3.4</version>
     <relativePath>../pom.xml</relativePath>
   </parent>
 

…lchecker/src/test/resources/beo-spec.cml core/analysis/modelchecker/beo-spec.cmlcore/analysis/modelchecker/src/test/resources/beo-spec.cml renamed to core/analysis/modelchecker/beo-spec.cml core/analysis/modelchecker/src/test/resources/beo-spec.cml renamed to core/analysis/modelchecker/beo-spec.cml

@@ -11,13 +11,10 @@
 
 public class FormulaIntegrationUtilities {
 
-	//public static final String WORKING_DIRECTORY = "src/test/resources";
-	//public static final String WORKING_DIRECTORY = FileSystemView.getFileSystemView().getHomeDirectory().getAbsolutePath();
-	public static final String BASIC_FORMULA_SCRIPT = "/basic_formula_script.fml";
-	
-	public static final String AUXILIARY_DEFINITIONS_SCRIPT = "/aux_definitions.fml";
+	public static final String AUXILIARY_DEFINITIONS_SCRIPT = "/cml_aux_definitions.fml";
 	public static final String SYNTAX_DOMAIN_SCRIPT = "/cml_syntax.fml";
 	public static final String SEMANTICS_DOMAIN_SCRIPT = "/cml_semantics.fml";
+	public static final String SEMANTICS_TIMED_DOMAIN_SCRIPT = "/cml_semantics_timed.fml";
 	public static final String PROPERTIES_DOMAIN_SCRIPT = "/cml_properties.fml";
 
 	public static void buildSpecification(String specificContent){
@@ -49,8 +46,4 @@ public static void writeScriptToFile(String filePath, StringBuilder content) thr
 		 bw.close();
 	 }
 
-	public static void main(String[] args) throws Exception{
-		String content = FormulaIntegrationUtilities.readScriptFromFile(BASIC_FORMULA_SCRIPT).toString();
-		System.out.println(content);
-	}
 }

core/analysis/modelchecker/pom.xml

@@ -30,6 +30,9 @@ public interface MCNode {
 
 	//the option to generate values by extension
 	public static final String EXTENSION = "EXTENSION";
+	
+	
+	public static final String STATE_DEPENDENCY_WITHOUT_INF_VARS = "STATE_DEPENDENCY_WITHOUT_INF_VARS";
 
 	public String toFormula(String option);
 

core/analysis/modelchecker/src/main/java/eu/compassresearch/core/analysis/modelchecker/api/FormulaIntegrationUtilities.java

@@ -1,15 +1,12 @@
 package eu.compassresearch.core.analysis.modelchecker.ast.actions;
 
-import java.util.Iterator;
 import java.util.LinkedList;
 
 import eu.compassresearch.core.analysis.modelchecker.ast.MCNode;
 import eu.compassresearch.core.analysis.modelchecker.ast.auxiliary.ActionChannelDependency;
 import eu.compassresearch.core.analysis.modelchecker.ast.auxiliary.ExpressionEvaluator;
 import eu.compassresearch.core.analysis.modelchecker.ast.auxiliary.MCCommEv;
 import eu.compassresearch.core.analysis.modelchecker.ast.auxiliary.MCLieInFact;
-import eu.compassresearch.core.analysis.modelchecker.ast.auxiliary.NameValue;
-import eu.compassresearch.core.analysis.modelchecker.ast.auxiliary.SingleTypeValue;
 import eu.compassresearch.core.analysis.modelchecker.ast.auxiliary.TypeManipulator;
 import eu.compassresearch.core.analysis.modelchecker.ast.auxiliary.TypeValue;
 import eu.compassresearch.core.analysis.modelchecker.ast.definitions.MCAActionDefinition;
@@ -127,9 +124,16 @@ public String toFormula(String option) {
 		} else{
 			//int i = 0;
 			//result.append(buildReplicatedExternalChoice(context, values, option, allParamsCopy,false));
+			
 			result.append(buildPrefix(option, context, false));
 
 		}
+		if(this.communicationParameters.size() > 0){
+			if(this.communicationParameters.getFirst() instanceof MCAReadCommunicationParameter){
+				String localVarName = this.communicationParameters.getFirst().toString();
+				context.localInputVariables.add(localVarName);
+			}
+		}
 		return result.toString();
 	}
 

core/analysis/modelchecker/src/main/java/eu/compassresearch/core/analysis/modelchecker/ast/MCNode.java

@@ -31,7 +31,6 @@ public MCAExternalChoiceReplicatedAction(
 
 	@Override
 	public String toFormula(String option) {
-		 
 		NewCMLModelcheckerContext context = NewCMLModelcheckerContext.getInstance();
 		MCPSingleDeclaration sDecl = this.getReplicationDeclaration().getFirst();
 		LinkedList<MCPCMLExp> indexes = new LinkedList<MCPCMLExp>();

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

@@ -3,11 +3,9 @@
 import java.util.LinkedList;
 
 import eu.compassresearch.core.analysis.modelchecker.ast.declarations.MCAExpressionSingleDeclaration;
-import eu.compassresearch.core.analysis.modelchecker.ast.declarations.MCATypeSingleDeclaration;
 import eu.compassresearch.core.analysis.modelchecker.ast.declarations.MCPSingleDeclaration;
 import eu.compassresearch.core.analysis.modelchecker.ast.expressions.MCASetEnumSetExp;
 import eu.compassresearch.core.analysis.modelchecker.ast.expressions.MCPCMLExp;
-import eu.compassresearch.core.analysis.modelchecker.ast.expressions.MCPVarsetExpression;
 import eu.compassresearch.core.analysis.modelchecker.ast.statements.MCAActionStm;
 import eu.compassresearch.core.analysis.modelchecker.ast.statements.MCPCMLStm;
 import eu.compassresearch.core.analysis.modelchecker.visitors.NewCMLModelcheckerContext;