Skip to content
GitLab
Commit e0d2b93d authored by Sudeep Kanav's avatar Sudeep Kanav
Browse files

renamed Module to NuSMVModule in the ecore file 

refs 3105
parent 1dce78f9
Hide whitespace changes
Inline Side-by-side
org.fortiss.af3.component/trunk/src/org/fortiss/af3/component/generator/nusmv/.ratings
View file @ e0d2b93d
AF3ToNuSMVConsts.java 5778ae07a01b235df7b43f4a7d27d069efd36b2e GREEN
ArrayToStructVariableDefinition.java 9fe1c7cb090d9e6a20c8f242d5f6453fd691c584 GREEN
CodeSpecPrepareAddReturnStatement.java 345452b4f08d0e41c5f8a9650310c9add2bad414 GREEN
......@@ -11,6 +10,6 @@ MultiValuedMap.java a48091f2a40ae06984f43a50a86cbc8e9bd8c5ba GREEN
NamesTransformation.java 278bdc970d5e14ee2b9035e4ca542c6122eb55a7 GREEN
ResolveNoVal.java 2d7727f4afaef58a54314f5a4d900e47bff9caa0 GREEN
StandaloneBooleanVarToFunctionCall.java 7d5c7458131b6c3bc82042bdbeec6973c2cece7d GREEN
ToNuSMVComponent.java 9a739adeec8cb96828833825d604e0d9abd31f43 GREEN
ToNuSMVDataDictionary.java 27df1e5bcbdd71c550e90b3687e656d7758c2024 GREEN
ToNuSMVExpression.java 7768f211b5299930bdb4d0156bb7c76677961806 GREEN
ToNuSMVComponent.java ecb72e63284accf8a74bcdf5cb097b31561f9335 YELLOW
ToNuSMVDataDictionary.java 3b44b3b3230cdf44d2b167996a7d8eb871f0ed07 YELLOW
ToNuSMVExpression.java d97e5860451ac72abf829a482f159a42e6c0d047 YELLOW
org.fortiss.af3.component/trunk/src/org/fortiss/af3/component/generator/nusmv/ToNuSMVComponent.java
View file @ e0d2b93d
......@@ -55,7 +55,7 @@ import org.fortiss.af3.project.model.FileProject;
import org.fortiss.af3.tools.nusmv.model.NuSMVFile;
import org.fortiss.af3.tools.nusmv.model.define.Define;
import org.fortiss.af3.tools.nusmv.model.module.LocalVariable;
import org.fortiss.af3.tools.nusmv.model.module.Module;
import org.fortiss.af3.tools.nusmv.model.module.NuSMVModule;
import org.fortiss.af3.tools.nusmv.model.types.EnumerationType;
import org.fortiss.af3.tools.nusmv.model.types.ModuleType;
import org.fortiss.af3.tools.nusmv.model.types.TypeBase;
......@@ -99,7 +99,7 @@ public class ToNuSMVComponent extends CacheSupportedTransformationBase {
/** Function to transform a component. To be made into a new class */
private Object transformComponent(Component comp,
IPragmaticTransformation deferredTransformation) {
Module module = createModule(comp.getName());
NuSMVModule module = createModule(comp.getName());
addToMap(comp, module);
NuSMVFile logicalFile =
(NuSMVFile)deferredTransformation.buildTransformation(getFileProject(comp));
......@@ -119,7 +119,7 @@ public class ToNuSMVComponent extends CacheSupportedTransformationBase {
private Object transformOutputPort(OutputPort op,
IPragmaticTransformation deferredTransformation) {
Component parentComponent = op.getComponent();
Module module = (Module)deferredTransformation.buildTransformation(parentComponent);
NuSMVModule module = (NuSMVModule)deferredTransformation.buildTransformation(parentComponent);
IExpressionTerm portInitVal = computeDefaultValueForType(op.getVariableType(), op);
......@@ -149,7 +149,7 @@ public class ToNuSMVComponent extends CacheSupportedTransformationBase {
transformInputPort(InputPort ip, IPragmaticTransformation deferredTransformation) {
Component parentComponent = ip.getComponent();
Module module = (Module)deferredTransformation.buildTransformation(parentComponent);
NuSMVModule module = (NuSMVModule)deferredTransformation.buildTransformation(parentComponent);
String nuSMVName = getNuSMVNameForNamedElement(ip);
TypeBase nuSMVType = getNuSMVType(ip);
......@@ -176,7 +176,7 @@ public class ToNuSMVComponent extends CacheSupportedTransformationBase {
}
/** Add an invariant in case of an atomic cycle that target is equal to the source. */
private static void addInVariantIfNeeded(Module module, Channel ch,
private static void addInVariantIfNeeded(NuSMVModule module, Channel ch,
IPragmaticTransformation deferredTransformation) {
if(ch.getSource().getComponent() == ch.getTarget().getComponent()) {
Object tmpSrc = deferredTransformation.buildTransformation(ch.getSource());
......@@ -208,7 +208,7 @@ public class ToNuSMVComponent extends CacheSupportedTransformationBase {
IPragmaticTransformation deferredTransformation) {
Component parentComponent = (Component)dsv.eContainer().eContainer();
Module module = (Module)deferredTransformation.buildTransformation(parentComponent);
NuSMVModule module = (NuSMVModule)deferredTransformation.buildTransformation(parentComponent);
String nuSMVName = getNuSMVName(dsv);
TypeBase nuSMVType = getNuSMVType(dsv);
IExpressionTerm initExp =
......@@ -223,11 +223,11 @@ public class ToNuSMVComponent extends CacheSupportedTransformationBase {
/** Transforms a hierarchical component. */
private static void transformHierarchicalComponent(Component comp,
IPragmaticTransformation deferredTransformation) {
Module module = (Module)deferredTransformation.buildTransformation(comp);
NuSMVModule module = (NuSMVModule)deferredTransformation.buildTransformation(comp);
// link the previous translations and the current component
for(Component subComp : comp.getSubComponents()) {
Module subModule =
(Module)deferredTransformation.buildTransformation(subComp,
NuSMVModule subModule =
(NuSMVModule)deferredTransformation.buildTransformation(subComp,
deferredTransformation);
ArrayList<IExpressionTerm> params = new ArrayList<IExpressionTerm>();
......@@ -291,6 +291,6 @@ public class ToNuSMVComponent extends CacheSupportedTransformationBase {
* Computes the name of the NuSMV variable that holds an instance of the component c.
*/
public static String getModuleInstanceName(Component c, IPragmaticTransformation dt) {
return ((Module)dt.buildTransformation(c)).getName() + VAR;
return ((NuSMVModule)dt.buildTransformation(c)).getName() + VAR;
}
}
org.fortiss.af3.component/trunk/src/org/fortiss/af3/component/generator/nusmv/ToNuSMVDataDictionary.java
View file @ e0d2b93d
......@@ -32,7 +32,7 @@ import org.fortiss.af3.expression.model.terms.imperative.IfThenElse;
import org.fortiss.af3.expression.model.terms.imperative.Return;
import org.fortiss.af3.tools.nusmv.model.NuSMVFile;
import org.fortiss.af3.tools.nusmv.model.module.LocalVariable;
import org.fortiss.af3.tools.nusmv.model.module.Module;
import org.fortiss.af3.tools.nusmv.model.module.NuSMVModule;
import org.fortiss.pragmatictransformation.service.CacheSupportedTransformationBase;
import org.fortiss.pragmatictransformation.service.IPragmaticTransformation;
......@@ -58,7 +58,7 @@ public class ToNuSMVDataDictionary extends CacheSupportedTransformationBase {
private Object transformFunctionDefinition(FunctionDefinition fd,
IPragmaticTransformation deferredTransformation) {
Module module = createModule(fd.getFunction().getName());
NuSMVModule module = createModule(fd.getFunction().getName());
addToMap(fd, module);
NuSMVFile logicalFile =
(NuSMVFile)deferredTransformation.buildTransformation(getFileProject(fd));
......
org.fortiss.af3.component/trunk/src/org/fortiss/af3/component/generator/nusmv/ToNuSMVExpression.java
View file @ e0d2b93d
......@@ -39,7 +39,7 @@ import org.fortiss.af3.project.model.typesystem.ITerm;
import org.fortiss.af3.project.model.typesystem.IVariableScope;
import org.fortiss.af3.tools.nusmv.model.exp.ConditionalExpression;
import org.fortiss.af3.tools.nusmv.model.module.LocalVariable;
import org.fortiss.af3.tools.nusmv.model.module.Module;
import org.fortiss.af3.tools.nusmv.model.module.NuSMVModule;
import org.fortiss.af3.tools.nusmv.model.types.ModuleType;
import org.fortiss.pragmatictransformation.service.CacheSupportedTransformationBase;
import org.fortiss.pragmatictransformation.service.IPragmaticTransformation;
......@@ -98,9 +98,9 @@ public class ToNuSMVExpression extends CacheSupportedTransformationBase {
if(scope == null)
scope = getFirstParentWithType(fc, FunctionDefinition.class);
Module module = (Module)deferredTransformation.buildTransformation(scope);
NuSMVModule module = (NuSMVModule)deferredTransformation.buildTransformation(scope);
Module functionModule = (Module)deferredTransformation.buildTransformation(obj);
NuSMVModule functionModule = (NuSMVModule)deferredTransformation.buildTransformation(obj);
ModuleType tpe = createModuleType(functionModule, actualParams);
LocalVariable lv = addLocalVariableIntoModule(module, tpe);
Var v = createVar(lv.getName() + "." + RESULT_NAME);
......@@ -117,7 +117,7 @@ public class ToNuSMVExpression extends CacheSupportedTransformationBase {
}
/** Adds a variable that represents a call to the module representing the function. */
private LocalVariable addLocalVariableIntoModule(Module module, ModuleType tpe) {
private LocalVariable addLocalVariableIntoModule(NuSMVModule module, ModuleType tpe) {
int index = 0;
for(LocalVariable lv : module.getVariables()) {
if(lv.getType() instanceof ModuleType) {
......
org.fortiss.af3.ocra/trunk/src/org/fortiss/af3/ocra/run/OCRARunner.java
View file @ e0d2b93d
......@@ -43,7 +43,7 @@ import org.fortiss.af3.tools.base.ToolRunnerBase;
import org.fortiss.af3.tools.base.UnknownLanguageFragmentException;
import org.fortiss.af3.tools.nusmv.model.NuSMVFile;
import org.fortiss.af3.tools.nusmv.model.NuSMVModelFactory;
import org.fortiss.af3.tools.nusmv.model.module.Module;
import org.fortiss.af3.tools.nusmv.model.module.NuSMVModule;
import org.fortiss.af3.tools.nusmv.model.run.NuSMVResult;
import org.fortiss.af3.tools.nusmv.run.ModelCheckingException;
import org.fortiss.af3.tools.nusmv.run.NuSMVRunner;
......@@ -75,7 +75,7 @@ public class OCRARunner extends ToolRunnerBase<Component, NuSMVResult> {
}
/** */
public NuSMVResult checkContractImplementation(Component c, Contract con, Module m)
public NuSMVResult checkContractImplementation(Component c, Contract con, NuSMVModule m)
throws UnknownLanguageFragmentException, ModelCheckingException {
try {
final File modelFile = materialiseModelFile(c);
......@@ -105,7 +105,7 @@ public class OCRARunner extends ToolRunnerBase<Component, NuSMVResult> {
List<String> opNames = new ArrayList<String>();
c.getOutputPorts().forEach(p -> opNames.add(p.getName()));
Module mainModule = f.getMainModule();
NuSMVModule mainModule = f.getMainModule();
for(String opName : opNames) {
NuSMVModelFactory.addDefine(mainModule, createLocalVariable(opName, null),
createLocalVariable("module." + opName, null));
......
org.fortiss.af3.specification/trunk/src/org/fortiss/af3/specification/constraint/DeterminismConstraint.java
View file @ e0d2b93d
......@@ -47,7 +47,7 @@ import org.fortiss.af3.state.model.StateAutomaton;
import org.fortiss.af3.state.model.TransitionSegment;
import org.fortiss.af3.tools.base.UnknownLanguageFragmentException;
import org.fortiss.af3.tools.nusmv.model.module.LocalVariable;
import org.fortiss.af3.tools.nusmv.model.module.Module;
import org.fortiss.af3.tools.nusmv.model.module.NuSMVModule;
import org.fortiss.af3.tools.nusmv.model.run.NuSMVResult;
import org.fortiss.af3.tools.nusmv.run.ModelCheckingException;
import org.fortiss.af3.tools.nusmv.run.Specification;
......@@ -73,7 +73,7 @@ public class DeterminismConstraint extends StateAutomatonConstraintBase {
// Transform, then only lookup the transformed components. Needed to copy file-project.
trans.buildTransformation(ProjectUtils.getFileProject(comp));
Module m = (Module)trans.buildTransformation(comp);
NuSMVModule m = (NuSMVModule)trans.buildTransformation(comp);
// TODO: #7618 make this use a variable instead of using a string
// TODO(VA) is the comment in the line above still valid? Seems like it has been taken into
// account
......
org.fortiss.af3.specification/trunk/src/org/fortiss/af3/specification/modelchecking/af3tonusmv/ModelCheckingAnalysis.java
View file @ e0d2b93d
......@@ -54,7 +54,7 @@ import org.fortiss.af3.tools.base.UnknownLanguageFragmentException;
import org.fortiss.af3.tools.nusmv.model.NuSMVModelFactory;
import org.fortiss.af3.tools.nusmv.model.exp.SetDefinitionExpression;
import org.fortiss.af3.tools.nusmv.model.module.LocalVariable;
import org.fortiss.af3.tools.nusmv.model.module.Module;
import org.fortiss.af3.tools.nusmv.model.module.NuSMVModule;
import org.fortiss.af3.tools.nusmv.model.run.NuSMVResult;
import org.fortiss.af3.tools.nusmv.run.EModelCheckingType;
import org.fortiss.af3.tools.nusmv.run.ModelCheckingException;
......@@ -144,7 +144,7 @@ public class ModelCheckingAnalysis {
ModelCheckingAnalysis mca = new ModelCheckingAnalysis(model);
Module m = mca.getNuSMVModule();
NuSMVModule m = mca.getNuSMVModule();
StateAutomaton sa = getStateAutomaton(model);
......@@ -227,8 +227,8 @@ public class ModelCheckingAnalysis {
}
/** returns the Module of the Component the MCA has been initialised with. */
private Module getNuSMVModule() {
return (Module)this.mcTransformation.buildTransformation(this.comp);
private NuSMVModule getNuSMVModule() {
return (NuSMVModule)this.mcTransformation.buildTransformation(this.comp);
}
/**
......
org.fortiss.af3.specification/trunk/src/org/fortiss/af3/specification/modelchecking/af3tonusmv/OCRAAnalysis.java
View file @ e0d2b93d
......@@ -21,7 +21,7 @@ import org.fortiss.af3.component.model.Component;
import org.fortiss.af3.ocra.model.contract.Contract;
import org.fortiss.af3.ocra.run.OCRARunner;
import org.fortiss.af3.tools.base.UnknownLanguageFragmentException;
import org.fortiss.af3.tools.nusmv.model.module.Module;
import org.fortiss.af3.tools.nusmv.model.module.NuSMVModule;
import org.fortiss.af3.tools.nusmv.model.run.NuSMVResult;
import org.fortiss.af3.tools.nusmv.run.ModelCheckingException;
import org.fortiss.pragmatictransformation.service.IPragmaticTransformation;
......@@ -111,8 +111,8 @@ public class OCRAAnalysis {
}
/** returns the Module of the Component the MCA has been initialised with. */
private Module getNuSMVModule() {
return (Module)this.nusmvTrans.buildTransformation(this.comp);
private NuSMVModule getNuSMVModule() {
return (NuSMVModule)this.nusmvTrans.buildTransformation(this.comp);
}
/** returns the Module of the Component the MCA has been initialised with. */
......
org.fortiss.af3.specification/trunk/test-src/test/org/fortiss/af3/specification/nusmv/transformation/STLTransformationTest.java
View file @ e0d2b93d
......@@ -28,7 +28,7 @@ import org.eclipse.emf.common.util.URI;
import org.fortiss.af3.project.model.FileProject;
import org.fortiss.af3.specification.modelchecking.af3tonusmv.NuSMVTransformations;
import org.fortiss.af3.tools.nusmv.model.NuSMVFile;
import org.fortiss.af3.tools.nusmv.model.module.Module;
import org.fortiss.af3.tools.nusmv.model.module.NuSMVModule;
import org.junit.Before;
import org.junit.Test;
......@@ -76,8 +76,8 @@ public class STLTransformationTest {
/** Test code spec parsing. */
@Test
public void testAllModulesAreCorrectlyGenerated() {
List<Module> lstOutput = getChildrenWithType(output, Module.class);
List<Module> lstTestData = getChildrenWithType(nusmvFileSTL, Module.class);
List<NuSMVModule> lstOutput = getChildrenWithType(output, NuSMVModule.class);
List<NuSMVModule> lstTestData = getChildrenWithType(nusmvFileSTL, NuSMVModule.class);
// Again assuming that lists will be in same order
System.out.println("Output: " + lstOutput.size() + " modules and test data has " +
......
org.fortiss.af3.state/trunk/src/org/fortiss/af3/state/generator/nusmv/.ratings
View file @ e0d2b93d
AddActionsForUnassignedPorts.java 9921e0215c6623002eb1e9244874bdf484900203 GREEN
CodeSpecificationToStateAutomata.java cbea0d69934579bf88a854fe3a198a90d4fb052e GREEN
CopyProject.java 5b631382ea7bf1ae7fd0f3f320b2a8ca75c3b801 GREEN
FlattenStructureExpression.java 1adf6ec26d577f22b8f07160ade602ff1cd967b3 GREEN
ResolveNoVal.java aa1685029ff1e56805396e25ead91c7a218d4533 GREEN
StronglyCausalToWeaklyCausalComponent.java cbfcef2dda777f4579d1c1a9cb7f94026849f982 GREEN
ToNuSMVStateAutomatonWeaklyCausal.java 9caa25e032a8612a16cbc3e9cf17936e15f7643a GREEN
ToNuSMVStateAutomatonWeaklyCausal.java 6620cd4a932e39cb8d8b9f5c07398fc2b17aa3c0 YELLOW
org.fortiss.af3.state/trunk/src/org/fortiss/af3/state/generator/nusmv/ToNuSMVStateAutomatonWeaklyCausal.java
View file @ e0d2b93d
......@@ -69,7 +69,7 @@ import org.fortiss.af3.tools.nusmv.model.exp.CaseFragment;
import org.fortiss.af3.tools.nusmv.model.exp.SetDefinitionExpression;
import org.fortiss.af3.tools.nusmv.model.exp.SetInclusionExpression;
import org.fortiss.af3.tools.nusmv.model.module.LocalVariable;
import org.fortiss.af3.tools.nusmv.model.module.Module;
import org.fortiss.af3.tools.nusmv.model.module.NuSMVModule;
import org.fortiss.af3.tools.nusmv.model.trans.NextExpression;
import org.fortiss.af3.tools.nusmv.model.trans.SingleTransition;
import org.fortiss.af3.tools.nusmv.model.trans.TransConstraint;
......@@ -118,7 +118,7 @@ public class ToNuSMVStateAutomatonWeaklyCausal extends CacheSupportedTransformat
}
/** Creates the next-transition designator variable in the NuSMV Module */
private LocalVariable createNextTransitionVariable(Module module, List<Transition> transitions,
private LocalVariable createNextTransitionVariable(NuSMVModule module, List<Transition> transitions,
State initState) {
Function<Transition, String> enumValueForTransition =
......@@ -169,7 +169,7 @@ public class ToNuSMVStateAutomatonWeaklyCausal extends CacheSupportedTransformat
}
/** Creates the expressions for maintaining the data state. */
private void setNextAssignments(Module module, List<Transition> transitions, LocalVariable ntv,
private void setNextAssignments(NuSMVModule module, List<Transition> transitions, LocalVariable ntv,
IPragmaticTransformation dTrans, List<OutputPort> outputPorts) {
// The component transformer adds the variable definitions and initiations but not the next
// assignments. Instead of an actual ASSIGN block we create a TRANS constraint because
......@@ -207,7 +207,7 @@ public class ToNuSMVStateAutomatonWeaklyCausal extends CacheSupportedTransformat
* done to improve the readability of the create NuSMV file by preventing long guard expressions
* in the Transition Invariant.
*/
private void createGuardIntermediates(Module module, List<TransitionSegment> transitions,
private void createGuardIntermediates(NuSMVModule module, List<TransitionSegment> transitions,
IPragmaticTransformation dTrans) {
for(TransitionSegment ts : transitions) {
Transition t = this.<Transition>resolveOne(ts);
......@@ -239,7 +239,7 @@ public class ToNuSMVStateAutomatonWeaklyCausal extends CacheSupportedTransformat
* enforcing constraints on the next-transition variable. The constraints are of the form
* {@code t = t_1 -> guard_t1 }.
*/
private void setTransitionInvars(Module module, LocalVariable nextTransitionVariable,
private void setTransitionInvars(NuSMVModule module, LocalVariable nextTransitionVariable,
List<TransitionSegment> transitions) {
for(TransitionSegment ts : transitions) {
Transition t = this.<Transition>resolveOne(ts);
......@@ -257,7 +257,7 @@ public class ToNuSMVStateAutomatonWeaklyCausal extends CacheSupportedTransformat
* The permission for the idle transitions is given iff none of the outgoing transitions can be
* taken, i.e. all of their guards evaluate to false.
*/
private void setIdleTransitionInvars(Module module, LocalVariable nextTranVar,
private void setIdleTransitionInvars(NuSMVModule module, LocalVariable nextTranVar,
List<State> states) {
for(State s : states) {
Function<TransitionSegment, Guard> getTransitionGuard =
......@@ -429,9 +429,9 @@ public class ToNuSMVStateAutomatonWeaklyCausal extends CacheSupportedTransformat
}
/** Adds the behavior specified by the af3 state automaton to the NuSMV Module. */
private Module mapStateAutomaton(StateAutomaton sa, IPragmaticTransformation t) {
private NuSMVModule mapStateAutomaton(StateAutomaton sa, IPragmaticTransformation t) {
Component parentComponent = sa.getComponent();
Module module = (Module)t.buildTransformation(parentComponent); // resolve
NuSMVModule module = (NuSMVModule)t.buildTransformation(parentComponent); // resolve
/** Cached list of AF3 states in the AF3 automaton. */
List<State> _states = sa.getRootState().getSubStates();
......
org.fortiss.af3.tools/trunk/model/nusmv.ecore
View file @ e0d2b93d
......@@ -3,15 +3,15 @@
xmlns:ecore="http://www.eclipse.org/emf/2002/Ecore" name="model" nsURI="http://www.fortiss.org/af3/tools/nusmv" nsPrefix="org-fortiss-af3-tools-nusmv">
<eClassifiers xsi:type="ecore:EClass" name="NuSMVFile" eSuperTypes="platform:/resource/org.fortiss.tooling.kernel/model/kernel.ecore#//INamedElement">
<eStructuralFeatures xsi:type="ecore:EReference" name="modules" upperBound="-1"
eType="#//module/Module" containment="true"/>
eType="#//module/NuSMVModule" containment="true"/>
<eStructuralFeatures xsi:type="ecore:EReference" name="mainModule" lowerBound="1"
eType="#//module/Module" containment="true"/>
eType="#//module/NuSMVModule" containment="true"/>
<eStructuralFeatures xsi:type="ecore:EReference" name="defines" upperBound="-1"
eType="#//cpp/CPPDefine" containment="true"/>
</eClassifiers>
<eSubpackages name="module" nsURI="http://www.fortiss.org/af3/tools/nusmv/module"
nsPrefix="org-fortiss-af3-tools-nusmv-module">
<eClassifiers xsi:type="ecore:EClass" name="Module" eSuperTypes="platform:/resource/org.fortiss.tooling.kernel/model/kernel.ecore#//INamedElement">
<eClassifiers xsi:type="ecore:EClass" name="NuSMVModule" eSuperTypes="platform:/resource/org.fortiss.tooling.kernel/model/kernel.ecore#//INamedElement">
<eStructuralFeatures xsi:type="ecore:EReference" name="parameters" upperBound="-1"
eType="#//module/LocalVariable" containment="true"/>
<eStructuralFeatures xsi:type="ecore:EReference" name="variables" upperBound="-1"
......@@ -73,7 +73,7 @@
</eClassifiers>
<eClassifiers xsi:type="ecore:EClass" name="ModuleType" eSuperTypes="#//types/TypeBase">
<eStructuralFeatures xsi:type="ecore:EReference" name="module" lowerBound="1"
eType="#//module/Module"/>
eType="#//module/NuSMVModule"/>
<eStructuralFeatures xsi:type="ecore:EReference" name="actualParams" upperBound="-1"
eType="ecore:EClass platform:/resource/org.fortiss.af3.expression/model/expression.ecore#//terms/IExpressionTerm"
containment="true"/>
......
org.fortiss.af3.tools/trunk/model/nusmv.genmodel
View file @ e0d2b93d
......@@ -18,17 +18,17 @@
</genClasses>
<nestedGenPackages prefix="AF3NuSMVModule" basePackage="org.fortiss.af3.tools.nusmv.model"
disposableProviderFactory="true" ecorePackage="nusmv.ecore#//module">
<genClasses image="false" ecoreClass="nusmv.ecore#//module/Module">
<genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference nusmv.ecore#//module/Module/parameters"/>
<genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference nusmv.ecore#//module/Module/variables"/>
<genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference nusmv.ecore#//module/Module/assignments"/>
<genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference nusmv.ecore#//module/Module/specification"/>
<genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference nusmv.ecore#//module/Module/defines"/>
<genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference nusmv.ecore#//module/Module/ltlSpecification"/>
<genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference nusmv.ecore#//module/Module/invars"/>
<genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference nusmv.ecore#//module/Module/trans"/>
<genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference nusmv.ecore#//module/Module/initConstrains"/>
<genFeatures createChild="false" ecoreFeature="ecore:EAttribute nusmv.ecore#//module/Module/symbolicConstants"/>
<genClasses ecoreClass="nusmv.ecore#//module/NuSMVModule">
<genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference nusmv.ecore#//module/NuSMVModule/parameters"/>
<genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference nusmv.ecore#//module/NuSMVModule/variables"/>
<genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference nusmv.ecore#//module/NuSMVModule/assignments"/>
<genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference nusmv.ecore#//module/NuSMVModule/specification"/>
<genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference nusmv.ecore#//module/NuSMVModule/defines"/>
<genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference nusmv.ecore#//module/NuSMVModule/ltlSpecification"/>
<genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference nusmv.ecore#//module/NuSMVModule/invars"/>
<genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference nusmv.ecore#//module/NuSMVModule/trans"/>
<genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference nusmv.ecore#//module/NuSMVModule/initConstrains"/>
<genFeatures createChild="false" ecoreFeature="ecore:EAttribute nusmv.ecore#//module/NuSMVModule/symbolicConstants"/>
</genClasses>
<genClasses ecoreClass="nusmv.ecore#//module/LocalVariable">
<genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference nusmv.ecore#//module/LocalVariable/type"/>
......
org.fortiss.af3.tools/trunk/src/org/fortiss/af3/tools/base/ToolRunnerBase.java
View file @ e0d2b93d
......@@ -57,14 +57,6 @@ import org.fortiss.tooling.kernel.model.INamedElement;
* @author ratiu
*/
public abstract class ToolRunnerBase<S extends INamedElement, T> implements IToolRunner<T> {
/**
* Whether the tool should be debugged. If DEBUG == true, then generated files are not deleted.
* Currently defaults to true, since errors are still common and it improves the immediate error
* analysis.
*/
public static boolean DEBUG = true;
/** The logical file on which the tool will be run. */
protected S logicalFile;
......@@ -227,17 +219,18 @@ public abstract class ToolRunnerBase<S extends INamedElement, T> implements IToo
String duration = new DecimalFormat("###.###").format(durationInMS);
info(plugin, "Run in " + duration + "s.");
// There are exactly 2 elements in "outputs"
List<String> normallines = outputs.get(0).get();
List<String> errlines = outputs.get(1).get();
if(exitValue != 0) {
logRuntimeError();
info(plugin, "Output: " + outputs.get(0).get());
info(plugin, "Error:" + outputs.get(1).get());
info(plugin, "Output: " + normallines);
info(plugin, "Error:" + normallines);
String ec = exitValue + " - " + interpretProcessExitValues(exitValue);
throw new Exception(getToolCommand() + " exited with code " + ec);
}
List<String> errlines = outputs.get(1).get();
List<String> normallines = outputs.get(0).get();
if(errlines != null && !errlines.isEmpty()) {
warning(plugin, "Output: " + normallines);
warning(plugin, "Error:" + errlines);
......
org.fortiss.af3.tools/trunk/src/org/fortiss/af3/tools/nusmv/model/.ratings
View file @ e0d2b93d
NuSMVModelAccessFacade.java c0f88b71de764b79988bf20e1c805dba43edb00f YELLOW
NuSMVModelFactory.java 2b8487d19020d86c592c8e66bdb0de45a7b4668d GREEN
NuSMVSpecialFeaturesUtils.java 2d553ff17c7865e89f8ac159ac8bf8d04cd00fe1 GREEN
NuSMVModelAccessFacade.java 7a399ada3aabea80142214832d4bf911f8d8214e YELLOW
NuSMVModelFactory.java ad03ad18bdeeb44e4125ece77ab12fb770be9f73 YELLOW
NuSMVSpecialFeaturesUtils.java 04dacfcc9fc6d8d021cf7dd9113d79f6cd225e6b YELLOW
org.fortiss.af3.tools/trunk/src/org/fortiss/af3/tools/nusmv/model/NuSMVModelAccessFacade.java
View file @ e0d2b93d
......@@ -19,7 +19,7 @@ import java.util.function.Predicate;
import org.fortiss.af3.tools.nusmv.model.define.Define;
import org.fortiss.af3.tools.nusmv.model.module.LocalVariable;
import org.fortiss.af3.tools.nusmv.model.module.Module;
import org.fortiss.af3.tools.nusmv.model.module.NuSMVModule;
/**
* Facade for accessing (reading and writing) the NuSMV model.
......@@ -32,7 +32,7 @@ public class NuSMVModelAccessFacade {
* Returns the {@link Define} from module for the variable if it exists or
* null if it does not exist.
*/
public static Define findDefine(Module module, String varName) {
public static Define findDefine(NuSMVModule module, String varName) {
return module.getDefines().stream().filter(d -> d.getVariable().getName().equals(varName))
.findFirst().orElse(null);
}
......@@ -41,7 +41,7 @@ public class NuSMVModelAccessFacade {
* Returns a {@link LocalVariable} with a given name from a module or null
* if it does not exist.
*/
public static LocalVariable findLocalVariable(Module module, String varName) {
public static LocalVariable findLocalVariable(NuSMVModule module, String varName) {
Predicate<LocalVariable> matchVarName = lv -> lv.getName().equals(varName);
return module.getVariables().stream().filter(matchVarName).findFirst().orElse(null);
}
......
org.fortiss.af3.tools/trunk/src/org/fortiss/af3/tools/nusmv/model/NuSMVModelFactory.java
View file @ e0d2b93d
......@@ -52,7 +52,7 @@ import org.fortiss.af3.tools.nusmv.model.ltlspec.U;
import org.fortiss.af3.tools.nusmv.model.ltlspec.X;
import org.fortiss.af3.tools.nusmv.model.module.AF3NuSMVModuleFactory;
import org.fortiss.af3.tools.nusmv.model.module.LocalVariable;
import org.fortiss.af3.tools.nusmv.model.module.Module;
import org.fortiss.af3.tools.nusmv.model.module.NuSMVModule;
import org.fortiss.af3.tools.nusmv.model.operators.AF3NuSMVOperatorsFactory;
import org.fortiss.af3.tools.nusmv.model.operators.SwConstOperator;
import org.fortiss.af3.tools.nusmv.model.operators.ToIntOperator;
......@@ -257,7 +257,7 @@ public class NuSMVModelFactory {
* Add a local variable to the module if it does not exist or returns the
* existing one.
*/
public static LocalVariable addLocalVariable(Module module, String varName, TypeBase tpe) {
public static LocalVariable addLocalVariable(NuSMVModule module, String varName, TypeBase tpe) {
LocalVariable lv = findLocalVariable(module, varName);
if(lv != null) {
return lv;
......@@ -271,19 +271,19 @@ public class NuSMVModelFactory {
/**
* Add a local Variable to the module that is not part of the module yet and returns the same
*/
public static LocalVariable addLocalVariable(Module module, LocalVariable lv) {
public static LocalVariable addLocalVariable(NuSMVModule module, LocalVariable lv) {
assert (findLocalVariable(module, lv.getName()) == null);
module.getVariables().add(lv);
return lv;
}
/** Add an INVAR to the module. */
public static void addInvar(Module module, Invar inv) {
public static void addInvar(NuSMVModule module, Invar inv) {
module.getInvars().add(inv);
}
/** Add a parameter to the module. */
public static LocalVariable addParameter(Module module, String varName, TypeBase tpe) {
public static LocalVariable addParameter(NuSMVModule module, String varName, TypeBase tpe) {
LocalVariable lv = AF3NuSMVModuleFactory.eINSTANCE.createLocalVariable();
lv.setName(varName);
lv.setType(tpe);
......@@ -292,7 +292,7 @@ public class NuSMVModelFactory {
}
/** Add an init statement to the module. */
public static void addInit(Module module, LocalVariable lv, IExpressionTerm initExp) {
public static void addInit(NuSMVModule module, LocalVariable lv, IExpressionTerm initExp) {
Assignment init = AF3NuSMVAssignFactory.eINSTANCE.createAssignment();
init.setType(AssignmentType.INIT_ASSIGNMENT);
init.setVar(lv);
......@@ -301,14 +301,14 @@ public class NuSMVModelFactory {
}
/** Creates a TRANS constraint and adds it to the module. */
public static TransConstraint createTrans(Module module) {
public static TransConstraint createTrans(NuSMVModule module) {
TransConstraint trans = AF3NuSMVTransFactory.eINSTANCE.createTransConstraint();
module.getTrans().add(trans);
return trans;
}
/** Creates an INIT constraint and adds it to the module. */
public static InitConstraint addInitConstraint(Module module, IExpressionTerm exp) {
public static InitConstraint addInitConstraint(NuSMVModule module, IExpressionTerm exp) {
InitConstraint init = AF3NuSMVConstraintsFactory.eINSTANCE.createInitConstraint();
module.getInitConstrains().add(init);
init.setExpression(copy(exp));
......@@ -339,8 +339,8 @@ public class NuSMVModelFactory {
}
/** Adds a {@link TransConstraint} to the module */
public static TransConstraint
addTrans(Module module, Stream<SingleTransition> singleTransitions) {
public static TransConstraint addTrans(NuSMVModule module,
Stream<SingleTransition> singleTransitions) {
TransConstraint trans = AF3NuSMVTransFactory.eINSTANCE.createTransConstraint();
singleTransitions.forEach(st -> trans.getSingleTransitions().add(st));
module.getTrans().add(trans);
......@@ -355,7 +355,7 @@ public class NuSMVModelFactory {
}
/** Adds a {@link TransConstraint} to the module */
public static TransConstraint addTrans(Module module, SingleTransition singleTransition) {
public static TransConstraint addTrans(NuSMVModule module, SingleTransition singleTransition) {
TransConstraint trans = AF3NuSMVTransFactory.eINSTANCE.createTransConstraint();
trans.getSingleTransitions().add(singleTransition);
module.getTrans().add(trans);
......@@ -371,7 +371,7 @@ public class NuSMVModelFactory {
}
/** Add a define declaration to the module. */
public static Define addDefine(Module module, LocalVariable lv, IExpressionTerm exp) {
public static Define addDefine(NuSMVModule module, LocalVariable lv, IExpressionTerm exp) {
Define define = AF3NuSMVDefineFactory.eINSTANCE.createDefine();
define.setVariable(lv);
define.setExpression(exp);
......@@ -380,7 +380,7 @@ public class NuSMVModelFactory {
}
/** Enriches a define statement from a module by adding a new conditional. */
public static Define enrichDefine(Module module, String varName, IExpressionTerm guardExp,