Commit cf16e651 authored by Simon Barner's avatar Simon Barner
Browse files

Move the following bits of NuSMV support to org.fortiss.af3.verification

* org.fortiss.af3.component.generator.nusmv
* org.fortiss.af3.expression.generator.nusmv
* org.fortiss.af3.state.generator.nusmv

Issue-Ref: 3861
Issue-Url: https://af3-developer.fortiss.org/issues/3861

Signed-off-by: Simon Barner's avatarSimon Barner <barner@fortiss.org>
parent 666de4d8
......@@ -52,7 +52,6 @@ Export-Package: org.fortiss.af3.component;uses:="org.osgi.framework,
org.fortiss.af3.expression.model.terms,
org.fortiss.tooling.kernel.extension,
org.fortiss.af3.generator.common.model.java",
org.fortiss.af3.component.generator.nusmv,
org.fortiss.af3.component.library; uses:="org.fortiss.af3.component.model,
org.fortiss.tooling.kernel.extension.data,
org.fortiss.tooling.kernel.model,
......
......@@ -309,62 +309,4 @@
</modelElementClass>
</modelElementCompositor>
</extension>
<extension
point="org.fortiss.pragmatictransformation.pragmaticTransformationProvider">
<transformationProvider
transformationName="flattenVariableDefs">
<transformation
transformation="org.fortiss.af3.component.generator.nusmv.FlattenVariableDefs"></transformation>
</transformationProvider>
<transformationProvider transformationName="codeSpecPrepareT0">
<transformation
transformation="org.fortiss.af3.component.generator.nusmv.CodeSpecPrepareAddReturnStatement">
</transformation>
</transformationProvider>
<transformationProvider transformationName="codeSpecPrepareT1">
<transformation
transformation="org.fortiss.af3.component.generator.nusmv.CodeSpecPrepareToIfElseBlock">
</transformation>
</transformationProvider>
<transformationProvider transformationName="codeSpecPrepareT2">
<transformation
transformation="org.fortiss.af3.component.generator.nusmv.CodeSpecPrepareToIfSequence">
</transformation>
</transformationProvider>
<transformationProvider transformationName="codeSpecPrepareT3">
<transformation
transformation="org.fortiss.af3.component.generator.nusmv.CodeSpecPrepareRemoveMultipleAssignments">
</transformation>
</transformationProvider>
<transformationProvider
transformationName="arrayToStructSmallStepA">
<transformation
transformation="org.fortiss.af3.component.generator.nusmv.ArrayToStructVariableDefinition">
</transformation>
</transformationProvider>
<transformationProvider
transformationName="resolveStandaloneBooleanVars">
<transformation
transformation="org.fortiss.af3.component.generator.nusmv.StandaloneBooleanVarToFunctionCall"></transformation>
</transformationProvider>
</extension>
<extension point="org.fortiss.pragmatictransformation.pragmaticTransformationProvider">
<transformationProvider transformationName="copyProject">
<transformation transformation="org.fortiss.af3.component.generator.nusmv.CopyProject"></transformation>
</transformationProvider>
<transformationProvider transformationName="toNuSMV">
<transformation transformation="org.fortiss.af3.component.generator.nusmv.ToNuSMVComponent"></transformation>
<transformation transformation="org.fortiss.af3.component.generator.nusmv.ToNuSMVDataDictionary"></transformation>
<transformation transformation="org.fortiss.af3.component.generator.nusmv.ToNuSMVExpression"></transformation>
</transformationProvider>
<transformationProvider transformationName="resolveNoVal">
<transformation transformation="org.fortiss.af3.component.generator.nusmv.ResolveNoVal"></transformation>
</transformationProvider>
<transformationProvider transformationName="namesTransformation">
<transformation transformation="org.fortiss.af3.component.generator.nusmv.NamesTransformation"></transformation>
</transformationProvider>
</extension>
</plugin>
AF3ToNuSMVConsts.java 873d75fa85215be06915a97ddcd760883dca56db GREEN
ArrayToStructVariableDefinition.java 796523020c2b817032bb989f56094404adf84946 GREEN
CodeSpecPrepareAddReturnStatement.java e6b0dc4e41e3d29a8326d0c48027bfb76f0288ec GREEN
CodeSpecPrepareRemoveMultipleAssignments.java 795880e1dd95d0a579572c435a9c4647fb1db39a GREEN
CodeSpecPrepareToIfElseBlock.java a4a0300700fa7c3f11bb0b0a9d06f7392026bfe4 GREEN
CodeSpecPrepareToIfSequence.java aa91a979a9c9ec4bbe92976fc6f94f7a0921f4ae GREEN
CopyProject.java 222c9f6e3adb6d6df48900604a7e76a6d079132f GREEN
FlattenVariableDefs.java 5bb7a8810d31c203878b048f5eaee001e181a4b6 GREEN
MultiValuedMap.java 9a92088a5d39dab3e64dfbb05db0507cb6e89b9a GREEN
NamesTransformation.java d499765e1d165be02536fd671c9af1f4ca170c03 GREEN
ResolveNoVal.java 072925bb14e304611ced7b862b84ea48b0334839 GREEN
StandaloneBooleanVarToFunctionCall.java aee7121ff24e8a4171ce5448c96c62e1c16c109f GREEN
ToNuSMVComponent.java a987ec39c7cd04353b08a82f07574da903287d7c GREEN
ToNuSMVDataDictionary.java 2fb96751171fe55fadedacda96b1bcb2d7947f13 GREEN
ToNuSMVExpression.java 9fc83ecd70237c43007db2b80e77b5031ca2d021 GREEN
/*-------------------------------------------------------------------------+
| Copyright 2015 fortiss GmbH |
| |
| Licensed under the Apache License, Version 2.0 (the "License"); |
| you may not use this file except in compliance with the License. |
| You may obtain a copy of the License at |
| |
| http://www.apache.org/licenses/LICENSE-2.0 |
| |
| Unless required by applicable law or agreed to in writing, software |
| distributed under the License is distributed on an "AS IS" BASIS, |
| WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. |
| See the License for the specific language governing permissions and |
| limitations under the License. |
+--------------------------------------------------------------------------*/
package org.fortiss.af3.component.generator.nusmv;
/**
* This class contains the constants used in the AF3 to NuSMV transformation.
*
*/
public class AF3ToNuSMVConsts {
/** The "present" variable name suffix. */
public static final String _PRESENT = "_PRESENT";
/** The suffix for the variable for module instantiations in nusmv. */
public static final String VAR = "Var";
/**
* Functions are modeled as modules in nusmv. Every such module has a variable called "res"
* representing the result of the function call.
*/
public static final String RESULT_NAME = "res";
/** The name of the current state variable in NuSMV model. */
public static final String CURRENT_STATE = "_current_state";
/** The name of the "next transition" variable in NuSMV model. */
public static final String NEXT_TRANSITION = "_next_t";
/**
* The name of the second element in an NuSMV enumeration type in the case of AF3 enumerations
* with a single element.
*/
public static final String FAKE_VALUE_NAME = "FAKE_VALUE";
}
/*-------------------------------------------------------------------------+
| Copyright 2015 fortiss GmbH |
| |
| Licensed under the Apache License, Version 2.0 (the "License"); |
| you may not use this file except in compliance with the License. |
| You may obtain a copy of the License at |
| |
| http://www.apache.org/licenses/LICENSE-2.0 |
| |
| Unless required by applicable law or agreed to in writing, software |
| distributed under the License is distributed on an "AS IS" BASIS, |
| WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. |
| See the License for the specific language governing permissions and |
| limitations under the License. |
+--------------------------------------------------------------------------*/
package org.fortiss.af3.component.generator.nusmv;
import static org.eclipse.emf.ecore.util.EcoreUtil.remove;
import static org.fortiss.af3.component.utils.BehaviorModelElementFactory.createDataStateVariable;
import static org.fortiss.af3.component.utils.ComponentModelElementFactory.createChannelAndAttach;
import static org.fortiss.af3.component.utils.ComponentModelElementFactory.createInputPortAndAttach;
import static org.fortiss.af3.component.utils.ComponentModelElementFactory.createOutputPortAndAttach;
import static org.fortiss.af3.expression.model.terms.impl.DefinedConstStaticImpl.NoVal;
import static org.fortiss.af3.expression.utils.ExpressionModelElementFactory.createDefinedType;
import static org.fortiss.af3.expression.utils.ExpressionUtils.getTypeDefinition;
import static org.fortiss.af3.expression.utils.ExpressionUtils.isArrayType;
import static org.fortiss.tooling.kernel.utils.EcoreUtils.copy;
import org.fortiss.af3.component.model.Channel;
import org.fortiss.af3.component.model.Component;
import org.fortiss.af3.component.model.InputPort;
import org.fortiss.af3.component.model.Port;
import org.fortiss.af3.component.model.behavior.common.DataStateVariable;
import org.fortiss.af3.component.model.behavior.common.IDataStateVariableProvider;
import org.fortiss.af3.expression.model.definitions.FunctionParameter;
import org.fortiss.af3.expression.model.definitions.Structure;
import org.fortiss.af3.expression.model.terms.DefinedConst;
import org.fortiss.af3.expression.model.terms.IExpressionTerm;
import org.fortiss.af3.expression.model.types.TDefinedType;
import org.fortiss.af3.project.model.typesystem.IType;
import org.fortiss.af3.project.model.typesystem.ITypeDefinition;
import org.fortiss.af3.project.model.typesystem.IVariableDefinition;
import org.fortiss.pragmatictransformation.service.CacheSupportedTransformationBase;
import org.fortiss.pragmatictransformation.service.IPragmaticTransformation;
/**
* First step of the ArraysToStructure transformation. The complete transformation is structured as
* 2 step sequential transformation:
* 1) First transformation is structured as a parallel transformation of 2 transformations spreading
* across Expression and Component plugin.
* 2) Converting array expressions to structure expressions.
*
* This class transforms ports, data state variables, and also creates the channels between the new
* ports. It is to be noted that after execution of this small step transformation the model could
* be dirty.
*
* TODO 8022: Do we really need to create @{link {@link IVariableDefinition}? Shouldn't we just
* change the type of the old variable definition?
*
*/
public class ArrayToStructVariableDefinition extends CacheSupportedTransformationBase {
/** {@inheritDoc} */
@Override
public Object transform(Object c, IPragmaticTransformation deferredTransformation) {
if(c instanceof Port) {
Port p = (Port)c;
if(!isArrayType(p.getVariableType())) {
return null;
}
ITypeDefinition td = ((TDefinedType)p.getVariableType()).getDef();
Structure s = (Structure)deferredTransformation.buildTransformation(td);
Port sPort = createStructurePortAndAttach(p, s);
sPort.setId(p.getId());
addToMap(p, sPort);
remove(p);
return sPort;
} else if(c instanceof DataStateVariable) {
DataStateVariable dsv = (DataStateVariable)c;
IType dsvType = dsv.getVariableType();
ITypeDefinition td = getTypeDefinition(dsvType, dsvType);
IExpressionTerm initVal = dsv.getInitialValue();
if(!isArrayType(dsvType)) {
return null;
}
Structure s = (Structure)deferredTransformation.buildTransformation(td);
// After the following statement the new data state variable will have type structure
// but the initial value is still an array constant, but it is fine array const is
// converted to struct const in next step of the transformation.
TDefinedType structType = createDefinedType(copy(s));
DataStateVariable ds =
createDataStateVariable(dsv.getIdentifier(), structType, copy(initVal));
addToMap(dsv, ds);
ds.setId(dsv.getId());
IDataStateVariableProvider provider = (IDataStateVariableProvider)dsv.eContainer();
provider.getDataStateVariables().remove(dsv);
provider.getDataStateVariables().add(ds);
remove(dsv);
return ds;
} else if(c instanceof Channel) {
Channel ch = (Channel)c;
Port srcTransformedPort =
(Port)deferredTransformation.buildTransformation(ch.getSource());
Port tgtTransformedPort =
(Port)deferredTransformation.buildTransformation(ch.getTarget());
if(srcTransformedPort != null && tgtTransformedPort != null) {
Component pc = ch.getParentComponent();
Channel newChannel =
createChannelAndAttach(pc, "", srcTransformedPort, tgtTransformedPort);
newChannel.setId(ch.getId());
remove(ch);
}
return null;
} else if(c instanceof FunctionParameter) {
// Note that this is an in-place transformation. This could also go to the expression
// plugin.
FunctionParameter fp = (FunctionParameter)c;
if(!isArrayType(fp.getVariableType())) {
return null;
}
ITypeDefinition td = ((TDefinedType)fp.getVariableType()).getDef();
Structure s = (Structure)deferredTransformation.buildTransformation(td);
fp.setType(createDefinedType(copy(s)));
return fp;
}
return null;
}
/**
* Creates a structure port for an array port and attaches is to the parent component.
*/
private Port createStructurePortAndAttach(Port p, Structure s) {
TDefinedType newPortType = createDefinedType(copy(s));
Component pc = p.getComponent();
String pName = p.getName();
DefinedConst nVal = copy(NoVal);
return p instanceof InputPort ? createInputPortAndAttach(pc, pName, newPortType, nVal)
: createOutputPortAndAttach(pc, pName, newPortType, nVal);
}
}
/*-------------------------------------------------------------------------+
| Copyright 2016 fortiss GmbH |
| |
| Licensed under the Apache License, Version 2.0 (the "License"); |
| you may not use this file except in compliance with the License. |
| You may obtain a copy of the License at |
| |
| http://www.apache.org/licenses/LICENSE-2.0 |
| |
| Unless required by applicable law or agreed to in writing, software |
| distributed under the License is distributed on an "AS IS" BASIS, |
| WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. |
| See the License for the specific language governing permissions and |
| limitations under the License. |
+--------------------------------------------------------------------------*/
package org.fortiss.af3.component.generator.nusmv;
import static org.fortiss.af3.component.utils.FormalAnalysisTransformationUtils.lastStatementIsReturn;
import static org.fortiss.tooling.kernel.utils.EcoreUtils.getChildrenWithType;
import org.fortiss.af3.component.model.behavior.code.CodeSpecification;
import org.fortiss.af3.expression.model.terms.imperative.StatementSequence;
import org.fortiss.af3.expression.model.terms.imperative.impl.ReturnStaticImpl;
import org.fortiss.af3.project.model.FileProject;
import org.fortiss.pragmatictransformation.service.CacheSupportedTransformationBase;
import org.fortiss.pragmatictransformation.service.IPragmaticTransformation;
/**
* This is a part of the transformation converting a {@link CodeSpecification} to a state
* automata, which is modeled in 5 steps. First 4 steps are transforming the
* {@link CodeSpecification} to an behaviorally equivalent {@link CodeSpecification} from which we
* can do a canonical transformation to a state automata. The steps are:
* 1) Adding a return statement at the end of the code specification if a
* return statement is not present.
* 2) After this transformation code spec is a nested if else conditions with both if and else block
* present, and each block containing a return.
* 3) Converts the sequence of if-else to a sequence of if with no else block. Each if block loosely
* corresponds to a transition in the resulting state automata.
* 4) Removes the multiple assignments to variable which might be occurring due to previous
* transformations.
* 5) Canonically transforming the {@link CodeSpecification} to a state automata.
*
* This class corresponds to the point 1. This is required because in some cases
* {@link CodeSpecification} might have a path without a return statement. Transformations identify
* the end of a block with the return statement.
*
*/
public class CodeSpecPrepareAddReturnStatement extends CacheSupportedTransformationBase {
/** {@inheritDoc} */
@Override
public Object transform(Object c, IPragmaticTransformation deferredTransformation) {
// TODO 3180 Currently every transformation starts with iterating over the file project.
// This can be and should be made better.
if(c instanceof FileProject) {
getChildrenWithType((FileProject)c, CodeSpecification.class)
.forEach(e -> deferredTransformation.buildTransformation(e));
return c;
} else if(c instanceof CodeSpecification) {
StatementSequence ss = ((CodeSpecification)c).getBody();
if(!(lastStatementIsReturn(ss.getStatements()))) {
ss.getStatements().add(ReturnStaticImpl.create());
}
}
return null;
}
}
/*-------------------------------------------------------------------------+
| Copyright 2016 fortiss GmbH |
| |
| Licensed under the Apache License, Version 2.0 (the "License"); |
| you may not use this file except in compliance with the License. |
| You may obtain a copy of the License at |
| |
| http://www.apache.org/licenses/LICENSE-2.0 |
| |
| Unless required by applicable law or agreed to in writing, software |
| distributed under the License is distributed on an "AS IS" BASIS, |
| WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. |
| See the License for the specific language governing permissions and |
| limitations under the License. |
+--------------------------------------------------------------------------*/
package org.fortiss.af3.component.generator.nusmv;
import static org.fortiss.tooling.kernel.utils.EcoreUtils.getChildrenWithType;
import java.util.ArrayList;
import java.util.HashMap;
import java.util.List;
import java.util.Map;
import org.fortiss.af3.component.model.behavior.code.CodeSpecification;
import org.fortiss.af3.expression.model.terms.IExpressionTerm;
import org.fortiss.af3.expression.model.terms.Var;
import org.fortiss.af3.expression.model.terms.imperative.Assignment;
import org.fortiss.af3.expression.model.terms.imperative.IStatementTerm;
import org.fortiss.af3.expression.model.terms.imperative.IfThenElse;
import org.fortiss.af3.expression.model.terms.imperative.StatementSequence;
import org.fortiss.af3.expression.model.terms.imperative.impl.ReturnStaticImpl;
import org.fortiss.af3.expression.utils.ExpressionModelElementFactory;
import org.fortiss.af3.project.model.FileProject;
import org.fortiss.pragmatictransformation.service.CacheSupportedTransformationBase;
import org.fortiss.pragmatictransformation.service.IPragmaticTransformation;
/**
* This is a part of the transformation converting a {@link CodeSpecification} to a state
* automata, which is modeled in 5 steps. First 4 steps are transforming the
* {@link CodeSpecification} to an behaviorally equivalent {@link CodeSpecification} from which we
* can do a canonical transformation to a state automata. The steps are:
* 1) Adding a return statement at the end of the code specification if a
* return statement is not present.
* 2) After this transformation code spec is a nested if else conditions with both if and else block
* present, and each block containing a return.
* 3) Converts the sequence of if-else to a sequence of if with no else block. Each if block loosely
* corresponds to a transition in the resulting state automata.
* 4) Removes the multiple assignments to variable which might be occurring due to previous
* transformations.
* 5) Canonically transforming the {@link CodeSpecification} to a state automata.
*
* This class corresponds to the point 4.
*
*/
public class CodeSpecPrepareRemoveMultipleAssignments extends CacheSupportedTransformationBase {
/** {@inheritDoc} */
@Override
public Object transform(Object c, IPragmaticTransformation deferredTransformation) {
if(c instanceof FileProject) {
getChildrenWithType((FileProject)c, CodeSpecification.class)
.forEach(e -> deferredTransformation.buildTransformation(e));
return c;
} else if(c instanceof CodeSpecification) {
CodeSpecification cs = (CodeSpecification)c;
removeMultiplePortAssignment(cs.getBody());
}
return null;
}
/**
* Input is assumed to be a list of if statements. It removes all the multiple assignments to a
* variable in the then blocks of if statements.
*/
private StatementSequence removeMultiplePortAssignment(StatementSequence ss) {
for(IStatementTerm s : ss.getStatements()) {
IfThenElse ifStatement = (IfThenElse)s;
ifStatement.setThenBlock(
removeMultiplePortAssignment(ifStatement.getThenBlock().getStatements()));
}
return ss;
}
/**
* This function takes a list of statements, which are assumed to be of the form of A*R, and
* removes multiple assignments to a variable. It keeps the last assignment only.
*/
private StatementSequence removeMultiplePortAssignment(List<IStatementTerm> ss) {
List<IStatementTerm> newStatements = new ArrayList<IStatementTerm>();
Map<Var, IExpressionTerm> assignmentMap = new HashMap<Var, IExpressionTerm>();
for(IStatementTerm s : ss) {
if(s instanceof Assignment) {
Assignment a = (Assignment)s;
assignmentMap.put(a.getVariable(), a.getValue());
}
}
for(Var v : assignmentMap.keySet()) {
newStatements.add(ExpressionModelElementFactory.assignment(v, assignmentMap.get(v)));
}
// Add the return statement at the last. The return statement in code spec does not returns
// a value.
newStatements.add(ReturnStaticImpl.create());
return ExpressionModelElementFactory.sequence(newStatements);
}
}
/*-------------------------------------------------------------------------+
| Copyright 2016 fortiss GmbH |
| |
| Licensed under the Apache License, Version 2.0 (the "License"); |
| you may not use this file except in compliance with the License. |
| You may obtain a copy of the License at |
| |
| http://www.apache.org/licenses/LICENSE-2.0 |
| |
| Unless required by applicable law or agreed to in writing, software |
| distributed under the License is distributed on an "AS IS" BASIS, |
| WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. |
| See the License for the specific language governing permissions and |
| limitations under the License. |
+--------------------------------------------------------------------------*/
package org.fortiss.af3.component.generator.nusmv;
import static org.fortiss.af3.component.utils.FormalAnalysisTransformationUtils.lastStatementIsReturn;
import static org.fortiss.tooling.kernel.utils.EcoreUtils.getChildrenWithType;
import java.util.ArrayList;
import java.util.List;
import java.util.Optional;
import org.eclipse.emf.ecore.util.EcoreUtil;
import org.fortiss.af3.component.model.behavior.code.CodeSpecification;
import org.fortiss.af3.expression.model.terms.imperative.IStatementTerm;
import org.fortiss.af3.expression.model.terms.imperative.IfThenElse;
import org.fortiss.af3.expression.model.terms.imperative.StatementSequence;
import org.fortiss.af3.expression.utils.ExpressionModelElementFactory;
import org.fortiss.af3.project.model.FileProject;
import org.fortiss.pragmatictransformation.service.CacheSupportedTransformationBase;
import org.fortiss.pragmatictransformation.service.IPragmaticTransformation;
/**
* This is a part of the transformation converting a {@link CodeSpecification} to a state
* automata, which is modeled in 5 steps. First 4 steps are transforming the
* {@link CodeSpecification} to an behaviorally equivalent {@link CodeSpecification} from which we
* can do a canonical transformation to a state automata. The steps are:
* 1) Adding a return statement at the end of the code specification if a
* return statement is not present.
* 2) After this transformation code spec is a nested if else conditions with both if and else block
* present, and each block containing a return.
* 3) Converts the sequence of if-else to a sequence of if with no else block. Each if block loosely
* corresponds to a transition in the resulting state automata.
* 4) Removes the multiple assignments to variable which might be occurring due to previous
* transformations.
* 5) Canonically transforming the {@link CodeSpecification} to a state automata.
*
* This class corresponds to the point 2. After this transformation code spec is a nested if else
* conditions with both if and else block present, and each block containing a return.
*
*/
public class CodeSpecPrepareToIfElseBlock extends CacheSupportedTransformationBase {
/** {@inheritDoc} */
@Override
public Object transform(Object c, IPragmaticTransformation deferredTransformation) {
if(c instanceof FileProject) {
getChildrenWithType((FileProject)c, CodeSpecification.class)
.forEach(e -> deferredTransformation.buildTransformation(e));
return c;
} else if(c instanceof CodeSpecification) {
// Convert this transformation to iterative transformation.
// TODO 3179 covert the transformation to iterative transformation
recursivelyApplyTransformation(((CodeSpecification)c).getBody());
// At this point code spec is a nested if else.
}
return null;
}
/**
* This function actually applies the transformation recursively.
*/
private void recursivelyApplyTransformation(StatementSequence ss) {
List<IStatementTerm> stList = ss.getStatements();
int i = indexOfFirstIfStatement(stList);
if(i == -1) {
return;
}
List<IStatementTerm> prefix = stList.subList(0, i);
List<IStatementTerm> suffix = stList.subList(i + 1, ss.getStatements().size());
IfThenElse ifStatement = (IfThenElse)stList.get(i);
List<IStatementTerm> thenBlockStatements = ifStatement.getThenBlock().getStatements();
List<IStatementTerm> elseBlockStatements = (ifStatement.getElseBlock() == null)
? new ArrayList<IStatementTerm>() : ifStatement.getElseBlock().getStatements();