From 33d910338223121836acdeed113c5605ab625d43 Mon Sep 17 00:00:00 2001 From: Tobias Wiessner Date: Tue, 15 Aug 2023 18:23:20 +0200 Subject: [PATCH 01/23] Add support for new property check for requirements called State-Recoverability --- .../ultimate/boogie/ExpressionFactory.java | 14 + .../core/lib/models/annotation/Check.java | 8 + .../preferences/UltimatePreferenceItem.java | 35 ++ trunk/source/PEAtoBoogie/META-INF/MANIFEST.MF | 1 + .../ultimate/pea2boogie/IReqSymbolTable.java | 6 + .../pea2boogie/PEAtoBoogieObserver.java | 19 +- .../VerificationResultTransformer.java | 10 +- .../RtInconcistencyConditionGenerator.java | 3 +- .../preferences/Pea2BoogiePreferences.java | 17 +- .../pea2boogie/req2pea/ReqCheckAnnotator.java | 100 ++++- .../ultimate/pea2boogie/results/ReqCheck.java | 37 +- .../ReqCheckStateRecoverabilityResult.java | 28 ++ .../staterecoverability/AuxStatement.java | 15 + .../AuxStatementContainer.java | 88 ++++ .../PeaPhaseProgramCounter.java | 59 +++ .../StateRecoverabilityAuxStatement.java | 124 ++++++ .../StateRecoverabilityGenerator.java | 392 ++++++++++++++++++ .../VerificationExpression.java | 74 ++++ .../VerificationExpressionContainer.java | 97 +++++ .../testgen/Req2CauseTrackingPea.java | 2 +- .../testgen/Req2ModifySymbolTablePea.java | 246 +++++++++++ .../Req2ModifySymbolTablePeaTransformer.java | 32 ++ .../translator/Req2BoogieTranslator.java | 13 +- .../translator/ReqSymboltableBuilder.java | 94 ++++- .../reqtotest/req/Req2TestReqSymbolTable.java | 17 +- 25 files changed, 1497 insertions(+), 34 deletions(-) create mode 100644 trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/results/ReqCheckStateRecoverabilityResult.java create mode 100644 trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/AuxStatement.java create mode 100644 trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/AuxStatementContainer.java create mode 100644 trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/PeaPhaseProgramCounter.java create mode 100644 trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/StateRecoverabilityAuxStatement.java create mode 100644 trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/StateRecoverabilityGenerator.java create mode 100644 trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/VerificationExpression.java create mode 100644 trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/VerificationExpressionContainer.java create mode 100644 trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/testgen/Req2ModifySymbolTablePea.java create mode 100644 trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/testgen/Req2ModifySymbolTablePeaTransformer.java diff --git a/trunk/source/Library-BoogieAST/src/de/uni_freiburg/informatik/ultimate/boogie/ExpressionFactory.java b/trunk/source/Library-BoogieAST/src/de/uni_freiburg/informatik/ultimate/boogie/ExpressionFactory.java index 75bc83a0da3..2e7f917b061 100644 --- a/trunk/source/Library-BoogieAST/src/de/uni_freiburg/informatik/ultimate/boogie/ExpressionFactory.java +++ b/trunk/source/Library-BoogieAST/src/de/uni_freiburg/informatik/ultimate/boogie/ExpressionFactory.java @@ -397,7 +397,21 @@ private static Expression constructBinExprWithLiteralOpsBitvector(final ILocatio throw new AssertionError("unknown operator " + operator); } } + + public static Expression constructIfThenExpression(final ILocation loc, final Expression condition, + final Expression thenPart) { + if (condition instanceof BooleanLiteral) { + final boolean value = ((BooleanLiteral) condition).getValue(); + if (value) { + return thenPart; + } + } + final BoogieType type = TypeCheckHelper.typeCheckIfThenElseExpression((BoogieType) condition.getType(), + (BoogieType) thenPart.getType(), (BoogieType) thenPart.getType(), new TypeErrorReporter(loc)); + return new IfThenElseExpression(loc, type, condition, thenPart, null); + } + public static Expression constructIfThenElseExpression(final ILocation loc, final Expression condition, final Expression thenPart, final Expression elsePart) { if (condition instanceof BooleanLiteral) { diff --git a/trunk/source/Library-UltimateCore/src/de/uni_freiburg/informatik/ultimate/core/lib/models/annotation/Check.java b/trunk/source/Library-UltimateCore/src/de/uni_freiburg/informatik/ultimate/core/lib/models/annotation/Check.java index 5def7bb39e8..5863c56bdfc 100644 --- a/trunk/source/Library-UltimateCore/src/de/uni_freiburg/informatik/ultimate/core/lib/models/annotation/Check.java +++ b/trunk/source/Library-UltimateCore/src/de/uni_freiburg/informatik/ultimate/core/lib/models/annotation/Check.java @@ -145,6 +145,10 @@ public enum Spec { * Check for requirements. Checks for incompleteness. */ INCOMPLETE, + /** + * Check for requirements. Checks for state recoverability. + */ + STATE_RECOVERABILITY, /** * Check if a petrified ICFG does provide enough thread instances. */ @@ -261,6 +265,8 @@ public static String getDefaultPositiveMessage(final Spec spec) { return "consistent"; case INCOMPLETE: return "complete"; + case STATE_RECOVERABILITY: + return "state recoverable"; case SUFFICIENT_THREAD_INSTANCES: return "petrification did provide enough thread instances (tool internal message, not intended for end users)"; case DATA_RACE: @@ -316,6 +322,8 @@ public static String getDefaultNegativeMessage(final Spec spec) { return "inconsistent"; case INCOMPLETE: return "incomplete"; + case STATE_RECOVERABILITY: + return "not recoverable"; case SUFFICIENT_THREAD_INSTANCES: return "petrification did not provide enough thread instances (tool internal message, not intended for end users)"; case DATA_RACE: diff --git a/trunk/source/Library-UltimateModel/src/de/uni_freiburg/informatik/ultimate/core/model/preferences/UltimatePreferenceItem.java b/trunk/source/Library-UltimateModel/src/de/uni_freiburg/informatik/ultimate/core/model/preferences/UltimatePreferenceItem.java index 69c322d6062..6fa7e6e2d52 100644 --- a/trunk/source/Library-UltimateModel/src/de/uni_freiburg/informatik/ultimate/core/model/preferences/UltimatePreferenceItem.java +++ b/trunk/source/Library-UltimateModel/src/de/uni_freiburg/informatik/ultimate/core/model/preferences/UltimatePreferenceItem.java @@ -28,6 +28,8 @@ import java.util.ArrayList; import java.util.List; +import java.util.regex.Matcher; +import java.util.regex.Pattern; import de.uni_freiburg.informatik.ultimate.core.model.IController; @@ -157,6 +159,7 @@ public interface IUltimatePreferenceItemValidator { IntegerValidator ONLY_POSITIVE = new IntegerValidator(0, Integer.MAX_VALUE); IntegerValidator ONLY_POSITIVE_NON_ZERO = new IntegerValidator(1, Integer.MAX_VALUE); IntegerValidator GEQ_TWO = new IntegerValidator(2, Integer.MAX_VALUE); + StringValidator EXPR_PAIR = new StringValidator("\\s{0,1}((\\w+)\\s*([<>=!][=]*)\\s*(\\w+))\\s{0,1}$"); boolean isValid(T value); @@ -203,6 +206,38 @@ public String getInvalidValueErrorMessage(final Double value) { return "Valid range is " + mMin + " <= value <= " + mMax; } } + + public class StringValidator implements IUltimatePreferenceItemValidator { + + private final String mPattern; + + public StringValidator(String pattern) { + mPattern = pattern; + } + + @Override + public boolean isValid(final String string) { + String[]exprPairs = string.split(","); + for(String exprPair : exprPairs) { + Matcher m = match(exprPair, mPattern); + if(!m.matches()) { + return false; + } + } + return true; + } + + @Override + public String getInvalidValueErrorMessage(final String string) { + return "Expression pairs " + string + " is not in the format VALUE, ...>"; + } + } + + default Matcher match(String s, String pattern) { + Pattern p = Pattern.compile(pattern); + Matcher m = p.matcher(s); + return m; + } } } diff --git a/trunk/source/PEAtoBoogie/META-INF/MANIFEST.MF b/trunk/source/PEAtoBoogie/META-INF/MANIFEST.MF index 9de87bad960..501aff82746 100644 --- a/trunk/source/PEAtoBoogie/META-INF/MANIFEST.MF +++ b/trunk/source/PEAtoBoogie/META-INF/MANIFEST.MF @@ -22,5 +22,6 @@ Require-Bundle: com.github.jhoenicke.javacup, de.uni_freiburg.informatik.ultimate.lib.automata Export-Package: de.uni_freiburg.informatik.ultimate.pea2boogie, de.uni_freiburg.informatik.ultimate.pea2boogie.results, + de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability, de.uni_freiburg.informatik.ultimate.pea2boogie.testgen Automatic-Module-Name: de.uni.freiburg.informatik.ultimate.pea2boogie diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/IReqSymbolTable.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/IReqSymbolTable.java index 6ddd49ed483..3785de49d80 100644 --- a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/IReqSymbolTable.java +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/IReqSymbolTable.java @@ -35,9 +35,11 @@ import de.uni_freiburg.informatik.ultimate.boogie.ast.Expression; import de.uni_freiburg.informatik.ultimate.boogie.ast.IdentifierExpression; import de.uni_freiburg.informatik.ultimate.boogie.ast.VariableLHS; +import de.uni_freiburg.informatik.ultimate.boogie.type.BoogieType; import de.uni_freiburg.informatik.ultimate.core.model.models.IBoogieType; import de.uni_freiburg.informatik.ultimate.lib.pea.PhaseEventAutomata; import de.uni_freiburg.informatik.ultimate.lib.srparse.pattern.PatternType; +import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.AuxStatementContainer; import de.uni_freiburg.informatik.ultimate.util.datastructures.UnionFind; public interface IReqSymbolTable { @@ -65,6 +67,10 @@ public interface IReqSymbolTable { Set getClockVars(); Set getStateVars(); + + Set getAuxVars(); + + AuxStatementContainer getAuxStatementContainer(); /** * Given a variable name, return the name of the primed version of this variable. diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/PEAtoBoogieObserver.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/PEAtoBoogieObserver.java index 8cedfe3eb2b..d36b66ec1c6 100644 --- a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/PEAtoBoogieObserver.java +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/PEAtoBoogieObserver.java @@ -15,6 +15,7 @@ import de.uni_freiburg.informatik.ultimate.pea2boogie.preferences.Pea2BoogiePreferences; import de.uni_freiburg.informatik.ultimate.pea2boogie.preferences.Pea2BoogiePreferences.PEATransformerMode; import de.uni_freiburg.informatik.ultimate.pea2boogie.testgen.Req2CauseTrackingPeaTransformer; +import de.uni_freiburg.informatik.ultimate.pea2boogie.testgen.Req2ModifySymbolTablePeaTransformer; import de.uni_freiburg.informatik.ultimate.pea2boogie.testgen.ReqTestResultUtil; import de.uni_freiburg.informatik.ultimate.pea2boogie.translator.Req2BoogieTranslator; @@ -55,6 +56,9 @@ private IElement generateBoogie(final List> patterns) { if (mode == PEATransformerMode.REQ_CHECK) { return generateReqCheckBoogie(patterns); } + if(mode == PEATransformerMode.REQ_PARAM_CHECK) { + return generateReqParamCheckBoogie(patterns); + } if (mode == PEATransformerMode.REQ_TEST) { return generateReqTestBoogie(patterns); } @@ -62,8 +66,7 @@ private IElement generateBoogie(final List> patterns) { } private IElement generateReqCheckBoogie(final List> patterns) { - final Req2BoogieTranslator translator = - new Req2BoogieTranslator(mServices, mLogger, patterns, Collections.emptyList()); + final Req2BoogieTranslator translator = new Req2BoogieTranslator(mServices, mLogger, patterns, Collections.emptyList()); final VerificationResultTransformer reporter = new VerificationResultTransformer(mLogger, mServices, translator.getReqSymbolTable()); // register CEX transformer that removes program executions from CEX. @@ -71,6 +74,18 @@ private IElement generateReqCheckBoogie(final List> patterns) { mServices.getResultService().registerTransformer("CexReducer", resultTransformer); return translator.getUnit(); } + + private IElement generateReqParamCheckBoogie(final List> patterns) { + final Req2ModifySymbolTablePeaTransformer transformer = new Req2ModifySymbolTablePeaTransformer(mServices, mLogger); + + final Req2BoogieTranslator translator = new Req2BoogieTranslator(mServices, mLogger, patterns, Collections.singletonList(transformer)); + + final VerificationResultTransformer reporter = new VerificationResultTransformer(mLogger, mServices, translator.getReqSymbolTable()); + // register CEX transformer that removes program executions from CEX. + final UnaryOperator resultTransformer = reporter::convertTraceAbstractionResult; + mServices.getResultService().registerTransformer("CexReducer", resultTransformer); + return translator.getUnit(); + } private IElement generateReqTestBoogie(final List> patterns) { // TODO: would it be nicer to get the symbol table via annotations? diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/VerificationResultTransformer.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/VerificationResultTransformer.java index c7db9cb43be..1f9903baadc 100644 --- a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/VerificationResultTransformer.java +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/VerificationResultTransformer.java @@ -95,6 +95,7 @@ import de.uni_freiburg.informatik.ultimate.pea2boogie.results.ReqCheck; import de.uni_freiburg.informatik.ultimate.pea2boogie.results.ReqCheckFailResult; import de.uni_freiburg.informatik.ultimate.pea2boogie.results.ReqCheckRtInconsistentResult; +import de.uni_freiburg.informatik.ultimate.pea2boogie.results.ReqCheckStateRecoverabilityResult; import de.uni_freiburg.informatik.ultimate.pea2boogie.results.ReqCheckSuccessResult; import de.uni_freiburg.informatik.ultimate.pea2boogie.translator.Req2BoogieTranslator; import de.uni_freiburg.informatik.ultimate.pea2boogie.translator.ReqSymboltableBuilder; @@ -153,7 +154,7 @@ public IResult convertTraceAbstractionResult(final IResult result) { final Spec spec = specs.iterator().next(); dieIfUnsupported(spec); - if (spec == Spec.CONSISTENCY || spec == Spec.VACUOUS) { + if (spec == Spec.CONSISTENCY || spec == Spec.VACUOUS || spec == Spec.STATE_RECOVERABILITY) { // a counterexample for consistency and vacuity means that the requirements are consistent or // non-vacuous isPositive = !isPositive; @@ -189,6 +190,12 @@ public IResult convertTraceAbstractionResult(final IResult result) { final String failurePath = formatTimeSequenceMap(delta2var2value); return new ReqCheckRtInconsistentResult<>(element, plugin, translatorSequence, failurePath); } + + if(spec == Spec.STATE_RECOVERABILITY) { + IBacktranslationService translatorSequenceStRec = oldRes.getCurrentBacktranslation(); + return new ReqCheckStateRecoverabilityResult<>(element, plugin, translatorSequenceStRec, reqCheck.getMessage()); + } + return new ReqCheckFailResult<>(element, plugin, translatorSequence); } @@ -557,6 +564,7 @@ private static void dieIfUnsupported(final Spec spec) { case CONSISTENCY: case VACUOUS: case RTINCONSISTENT: + case STATE_RECOVERABILITY: return; default: throw new UnsupportedOperationException("Unknown spec type " + spec); diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/generator/RtInconcistencyConditionGenerator.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/generator/RtInconcistencyConditionGenerator.java index d600d308dbc..09388596c13 100644 --- a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/generator/RtInconcistencyConditionGenerator.java +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/generator/RtInconcistencyConditionGenerator.java @@ -307,7 +307,8 @@ private static Script buildSolver(final IUltimateServiceProvider services) throw * */ public Expression generateNonDeadlockCondition(final PhaseEventAutomata[] automata) { - if (PRINT_PEA_DOT) { + //if (PRINT_PEA_DOT) { + if (true) { mLogger.info("### Printing DOT for Peas ###"); for (int i = 0; i < automata.length; ++i) { final PhaseEventAutomata pea = automata[i]; diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/preferences/Pea2BoogiePreferences.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/preferences/Pea2BoogiePreferences.java index 24452b7dbc4..703e8513440 100644 --- a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/preferences/Pea2BoogiePreferences.java +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/preferences/Pea2BoogiePreferences.java @@ -57,7 +57,7 @@ public class Pea2BoogiePreferences extends UltimatePreferenceInitializer { public static final String LABEL_CHECK_RT_INCONSISTENCY = "Check rt-inconsistency"; private static final boolean DEF_CHECK_RT_INCONSISTENCY = true; private static final String DESC_CHECK_RT_INCONSISTENCY = null; - + public static final String LABEL_USE_EPSILON = "Use epsilon transformation during rt-inconsistency check"; private static final boolean DEF_USE_EPSILON = true; private static final String DESC_USE_EPSILON = null; @@ -81,6 +81,14 @@ public class Pea2BoogiePreferences extends UltimatePreferenceInitializer { + " are treated as separate requirements. If enabled, each rt-inconsistency check is of the form " + "Invariants ∧ (check over all remaining requirements). If disabled, invariants are not treated separately."; + public static final String LABEL_CHECK_STATE_RECOVERABILITY = "Check state recoverability"; + private static final boolean DEF_CHECK_STATE_RECOVERABILITY = true; + private static final String DESC_CHECK_STATE_RECOVERABILITY = null; + + public static final String LABEL_STATE_RECOVERABILITY_VER_EXPR = "State recoverability expressions"; + private static final String DEF_STATE_RECOVERABILITY_VER_EXPR = "ENG_READY==true, ENG_START==false"; + private static final String DESC_STATE_RECOVERABILITY_VER_STRING = "Enter the expressions for which state recoverability should be valid"; + public static final String LABEL_GUESS_IN_OUT = "Use heuristic to find input/output definitions (if none are given)"; private static final boolean DEF_GUESS_IN_OUT = true; @@ -99,7 +107,7 @@ public class Pea2BoogiePreferences extends UltimatePreferenceInitializer { + "step independend of length or usefulness."; public enum PEATransformerMode { - REQ_CHECK, REQ_TEST + REQ_CHECK, REQ_PARAM_CHECK, REQ_TEST } public Pea2BoogiePreferences() { @@ -128,6 +136,11 @@ protected UltimatePreferenceItem[] initDefaultPreferences() { new UltimatePreferenceItem<>(LABEL_RT_INCONSISTENCY_USE_ALL_INVARIANTS, DEF_RT_INCONSISTENCY_USE_ALL_INVARIANTS, DESC_RT_INCONSISTENCY_USE_ALL_INVARIANTS, PreferenceType.Boolean), + new UltimatePreferenceItem<>(LABEL_CHECK_STATE_RECOVERABILITY, DEF_CHECK_STATE_RECOVERABILITY, DESC_CHECK_STATE_RECOVERABILITY, + PreferenceType.Boolean), + new UltimatePreferenceItem<>(LABEL_STATE_RECOVERABILITY_VER_EXPR, DEF_STATE_RECOVERABILITY_VER_EXPR, + DESC_STATE_RECOVERABILITY_VER_STRING, PreferenceType.String, + IUltimatePreferenceItemValidator.EXPR_PAIR), new UltimatePreferenceItem<>(LABEL_GUESS_IN_OUT, DEF_GUESS_IN_OUT, DESC_GUESS_IN_OUT, PreferenceType.Boolean), new UltimatePreferenceItem<>(LABEL_GUESS_INITIAL, DEF_GUESS_INITIAL, DESC_GUESS_INITIAL, diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/req2pea/ReqCheckAnnotator.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/req2pea/ReqCheckAnnotator.java index 89e5190ee98..23b95b24b5c 100644 --- a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/req2pea/ReqCheckAnnotator.java +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/req2pea/ReqCheckAnnotator.java @@ -31,6 +31,8 @@ import java.util.Collections; import java.util.Iterator; import java.util.List; +import java.util.Map; +import java.util.Optional; import java.util.Map.Entry; import java.util.Set; import java.util.concurrent.TimeUnit; @@ -47,6 +49,10 @@ import de.uni_freiburg.informatik.ultimate.boogie.ast.IntegerLiteral; import de.uni_freiburg.informatik.ultimate.boogie.ast.NamedAttribute; import de.uni_freiburg.informatik.ultimate.boogie.ast.Statement; +import de.uni_freiburg.informatik.ultimate.boogie.ast.UnaryExpression; +import de.uni_freiburg.informatik.ultimate.boogie.ast.BinaryExpression.Operator; +import de.uni_freiburg.informatik.ultimate.boogie.type.BoogiePrimitiveType; +import de.uni_freiburg.informatik.ultimate.boogie.type.BoogieType; import de.uni_freiburg.informatik.ultimate.core.lib.exceptions.RunningTaskInfo; import de.uni_freiburg.informatik.ultimate.core.lib.exceptions.ToolchainCanceledException; import de.uni_freiburg.informatik.ultimate.core.lib.models.annotation.Check; @@ -60,6 +66,7 @@ import de.uni_freiburg.informatik.ultimate.lib.pea.Phase; import de.uni_freiburg.informatik.ultimate.lib.pea.PhaseBits; import de.uni_freiburg.informatik.ultimate.lib.pea.PhaseEventAutomata; +import de.uni_freiburg.informatik.ultimate.lib.pea.modelchecking.DotWriterNew; import de.uni_freiburg.informatik.ultimate.lib.srparse.Durations; import de.uni_freiburg.informatik.ultimate.lib.srparse.pattern.PatternType; import de.uni_freiburg.informatik.ultimate.lib.srparse.pattern.PatternType.ReqPeas; @@ -70,6 +77,11 @@ import de.uni_freiburg.informatik.ultimate.pea2boogie.generator.RtInconcistencyConditionGenerator.InvariantInfeasibleException; import de.uni_freiburg.informatik.ultimate.pea2boogie.preferences.Pea2BoogiePreferences; import de.uni_freiburg.informatik.ultimate.pea2boogie.results.ReqCheck; +import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.AuxStatementContainer; +import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.PeaPhaseProgramCounter; +import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.StateRecoverabilityAuxStatement; +import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.StateRecoverabilityGenerator; +import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.VerificationExpression; import de.uni_freiburg.informatik.ultimate.pea2boogie.translator.CheckedReqLocation; import de.uni_freiburg.informatik.ultimate.util.CoreUtil; import de.uni_freiburg.informatik.ultimate.util.datastructures.CrossProducts; @@ -94,6 +106,7 @@ public class ReqCheckAnnotator implements IReq2PeaAnnotator { private int mCombinationNum; private boolean mCheckConsistency; private boolean mReportTrivialConsistency; + private boolean mCheckStateRecoverability; private boolean mSeparateInvariantHandling; private RtInconcistencyConditionGenerator mRtInconcistencyConditionGenerator; @@ -134,6 +147,8 @@ public List getStateChecks() { mReportTrivialConsistency = prefs.getBoolean(Pea2BoogiePreferences.LABEL_REPORT_TRIVIAL_RT_CONSISTENCY); mSeparateInvariantHandling = prefs.getBoolean(Pea2BoogiePreferences.LABEL_RT_INCONSISTENCY_USE_ALL_INVARIANTS); + mCheckStateRecoverability = prefs.getBoolean(Pea2BoogiePreferences.LABEL_CHECK_STATE_RECOVERABILITY); + // log preferences mLogger.info(String.format("%s=%s, %s=%s, %s=%s, %s=%s, %s=%s", Pea2BoogiePreferences.LABEL_CHECK_VACUITY, mCheckVacuity, Pea2BoogiePreferences.LABEL_RT_INCONSISTENCY_RANGE, mCombinationNum, @@ -171,8 +186,57 @@ private List generateAnnotations() { annotations.addAll(genChecksNonVacuity(mUnitLocation)); } annotations.addAll(genChecksRTInconsistency(mUnitLocation)); + //New check + if(mCheckStateRecoverability) { + annotations.addAll(genCheckStateRecoverability(mUnitLocation)); + } + return annotations; } + + private List genCheckStateRecoverability(final BoogieLocation bl) { + List list = new ArrayList<>(); + StateRecoverabilityGenerator mStRecGen = new StateRecoverabilityGenerator(); + //Set consideredPcLocations = mStRecGen.getRelevantLocationsFromPea(mReqPeas); + AuxStatementContainer auxStatementContainer = mSymbolTable.getAuxStatementContainer(); + Map>> vePeaAuxStatementMap = mStRecGen.getAuxStatementPerVerificationExpression(auxStatementContainer); + + for(Map.Entry>> entry : vePeaAuxStatementMap.entrySet()) { + VerificationExpression ve = entry.getKey(); + + for(Map.Entry> entryPeaStRecAuxSt : entry.getValue().entrySet()) { + Set stRecAuxStSet = entryPeaStRecAuxSt.getValue(); + for(StateRecoverabilityAuxStatement stRecAuxSt : stRecAuxStSet) { + String checkLabel = "STATE_RECOVERABILITY_" + entry.getKey().getVariable() + "_" + stRecAuxSt.getPcVariable(); + + Expression globalVariableTrue = mStRecGen.createExpression(bl, BoogieType.TYPE_BOOL, stRecAuxSt.getRelatedVariable(), Operator.COMPEQ, "true"); + Expression inputCondition = mStRecGen.createExpression(bl, BoogiePrimitiveType.toPrimitiveType(ve.getDataType()), ve.getVariable(), ve.getOperator(), ve.getValue()); + Expression andCondition = ExpressionFactory.newBinaryExpression(bl, Operator.LOGICAND, globalVariableTrue, inputCondition); + Expression expr = ExpressionFactory.constructUnaryExpression(bl, UnaryExpression.Operator.LOGICNEG, andCondition); + + final ReqCheck check = createReqCheck(Spec.STATE_RECOVERABILITY, stRecAuxSt.getPeaPhasePc().getReq(), entryPeaStRecAuxSt.getKey(), String.join("", ve.getExpr())); + list.add(createAssert(expr, check, checkLabel)); + } + } + } + + // DOT printen + final List, PhaseEventAutomata>> counterTracePEAList = new ArrayList<>(); + for (final ReqPeas reqPea : mReqPeas) { + //Pattern mit Anforderung als Key + final PatternType pattern = reqPea.getPattern(); + + //Nötig weil komplexere Anforderungen mehrere DC haben können + for (final Entry pea : reqPea.getCounterTrace2Pea()) { + counterTracePEAList.add(new Pair<>(pattern, pea.getValue())); + } + } + final List, PhaseEventAutomata>[]> subsets = CrossProducts.subArrays(counterTracePEAList.toArray(new Entry[counterTracePEAList.size()]), counterTracePEAList.size(), new Entry[counterTracePEAList.size()]); + //Prints parallel automaton + //dotPrinter(subsets); + + return list; + } private static List genCheckConsistency(final BoogieLocation bl) { final ReqCheck check = new ReqCheck(Spec.CONSISTENCY); @@ -255,7 +319,7 @@ private Statement genAssertRTInconsistency(final Entry, PhaseEven final PhaseEventAutomata[] automata = automataSet.toArray(new PhaseEventAutomata[subset.length]); final Expression expr = mRtInconcistencyConditionGenerator.generateNonDeadlockCondition(automata); - final ReqCheck check = createReqCheck(Spec.RTINCONSISTENT, subset); + final ReqCheck check = createReqCheck(Spec.RTINCONSISTENT,"", subset); if (expr == null) { if (mReportTrivialConsistency) { @@ -366,7 +430,7 @@ private Statement genAssertNonVacuous(final PatternType req, final PhaseEvent } @SafeVarargs - private static ReqCheck createReqCheck(final Check.Spec reqSpec, + private static ReqCheck createReqCheck(final Check.Spec reqSpec, final String message, final Entry, PhaseEventAutomata>... req2pea) { if (req2pea == null || req2pea.length == 0) { throw new IllegalArgumentException("subset cannot be null or empty"); @@ -379,11 +443,15 @@ private static ReqCheck createReqCheck(final Check.Spec reqSpec, peaNames[i] = req2pea[i].getValue().getName(); } - return new ReqCheck(reqSpec, reqIds, peaNames); + return new ReqCheck(reqSpec, reqIds, peaNames, message); } + private static ReqCheck createReqCheck(final Spec spec, final PatternType req, final PhaseEventAutomata aut, String message) { + return createReqCheck(spec, message, new Pair<>(req, aut)); + } + private static ReqCheck createReqCheck(final Spec spec, final PatternType req, final PhaseEventAutomata aut) { - return createReqCheck(spec, new Pair<>(req, aut)); + return createReqCheck(spec, "", new Pair<>(req, aut)); } /** @@ -412,6 +480,30 @@ private Expression genComparePhaseCounter(final int phaseIndex, final String pcN final IntegerLiteral intLiteral = ExpressionFactory.createIntegerLiteral(bl, Integer.toString(phaseIndex)); return ExpressionFactory.newBinaryExpression(bl, BinaryExpression.Operator.COMPEQ, identifier, intLiteral); } + + private void dotPrinter(final List, PhaseEventAutomata>[]> subsets) { + for(final Entry, PhaseEventAutomata>[] subset : subsets) { + + final Set automataSet = Arrays.stream(subset).map(Entry, PhaseEventAutomata>::getValue).collect(Collectors.toSet()); + assert automataSet.size() == subset.length; + final PhaseEventAutomata[] automata = automataSet.toArray(new PhaseEventAutomata[subset.length]); + + mLogger.info("### Printing DOT for Peas ###"); + for (int i = 0; i < automata.length; ++i) { + final PhaseEventAutomata pea = automata[i]; + mLogger.info(pea.getName() + CoreUtil.getPlatformLineSeparator() + DotWriterNew.createDotString(pea)); + } + if (automata.length < 8) { + final Optional prod = Arrays.stream(automata).reduce(PhaseEventAutomata::parallel); + if (prod.isPresent()) { + mLogger.info( + "PRODUCT" + CoreUtil.getPlatformLineSeparator() + DotWriterNew.createDotString(prod.get())); + } + } + mLogger.info("### Finished printing DOT ###"); + } + + } @Override public List getPreChecks() { diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/results/ReqCheck.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/results/ReqCheck.java index a3d8aa03630..ebbec7a25e5 100644 --- a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/results/ReqCheck.java +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/results/ReqCheck.java @@ -53,27 +53,34 @@ public class ReqCheck extends Check { private final String[] mReqIds; private final String[] mPeaNames; + + private final String mMessage; public ReqCheck(final Check.Spec type) { - this(EnumSet.of(type), 0, 0, new String[0], new String[0]); + this(EnumSet.of(type), 0, 0, new String[0], new String[0], ""); } + public ReqCheck(final Check.Spec type, final String[] reqIds, final String[] peaNames, String message) { + this(EnumSet.of(type), reqIds, peaNames, message); + } + public ReqCheck(final Check.Spec type, final String[] reqIds, final String[] peaNames) { - this(EnumSet.of(type), reqIds, peaNames); + this(EnumSet.of(type), reqIds, peaNames, ""); } - private ReqCheck(final EnumSet types, final String[] reqIds, final String[] peaNames) { - this(types, -1, -1, reqIds, peaNames); + private ReqCheck(final EnumSet types, final String[] reqIds, final String[] peaNames, String message) { + this(types, -1, -1, reqIds, peaNames, message); } private ReqCheck(final EnumSet types, final int startline, final int endline, final String[] reqIds, - final String[] peaNames) { + final String[] peaNames, String message) { super(types, a -> ReqCheck.getCustomPositiveMessage(a, reqIds, peaNames), a -> ReqCheck.getCustomNegativeMessage(a, reqIds, peaNames)); mStartline = startline; mEndline = endline; mReqIds = reqIds; mPeaNames = peaNames; + mMessage = message; } public int getStartLine() { @@ -128,7 +135,15 @@ public ReqCheck merge(final ReqCheck other) { final int endline = Math.max(mEndline, other.mEndline); final String[] reqIds = DataStructureUtils.concat(mReqIds, other.mReqIds); final String[] peaNames = DataStructureUtils.concat(mPeaNames, other.mPeaNames); - return new ReqCheck(newSpec, startline, endline, reqIds, peaNames); + final String message = mMessage.concat(other.getMessage()); + return new ReqCheck(newSpec, startline, endline, reqIds, peaNames, message); + } + + private String createMessage() { + if(mMessage.isEmpty()) { + return ""; + } + return mMessage; } public Set getReqIds() { @@ -138,13 +153,17 @@ public Set getReqIds() { public Set getPeaNames() { return new LinkedHashSet<>(Arrays.asList(mPeaNames)); } + + public String getMessage( ) { + return mMessage; + } @Override public String toString() { if (mReqIds.length == 0) { return super.toString() + " for all requirements"; } - return super.toString() + " for " + Arrays.stream(mReqIds).collect(Collectors.joining(", ")); + return super.toString() + " for " + Arrays.stream(mReqIds).collect(Collectors.joining(", ")) + " " + createMessage(); } @Override @@ -154,6 +173,7 @@ public int hashCode() { result = prime * result + mEndline; result = prime * result + Arrays.hashCode(mReqIds); result = prime * result + Arrays.hashCode(mPeaNames); + result = prime * result + mMessage.hashCode(); result = prime * result + mStartline; return result; } @@ -182,6 +202,9 @@ public boolean equals(final Object obj) { if (!Arrays.equals(mPeaNames, other.mPeaNames)) { return false; } + if(!mMessage.equalsIgnoreCase(other.getMessage())) { + return false; + } return true; } diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/results/ReqCheckStateRecoverabilityResult.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/results/ReqCheckStateRecoverabilityResult.java new file mode 100644 index 00000000000..60dfcb766df --- /dev/null +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/results/ReqCheckStateRecoverabilityResult.java @@ -0,0 +1,28 @@ +package de.uni_freiburg.informatik.ultimate.pea2boogie.results; + +import de.uni_freiburg.informatik.ultimate.core.model.models.IElement; +import de.uni_freiburg.informatik.ultimate.core.model.services.IBacktranslationService; +import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.structure.IAction; +import de.uni_freiburg.informatik.ultimate.util.CoreUtil; + +public class ReqCheckStateRecoverabilityResult extends ReqCheckFailResult { + + private final String mMessage; + + public ReqCheckStateRecoverabilityResult(final LOC element, final String plugin, final IBacktranslationService translatorSequence, final String message) { + super(element, plugin, translatorSequence); + mMessage = message; + } + + @Override + public String getLongDescription() { + final StringBuilder sb = new StringBuilder(); + sb.append(getShortDescription()); + sb.append(CoreUtil.getPlatformLineSeparator()); + if (mMessage != null) { + sb.append("Verification Expression: "); + sb.append(mMessage); + } + return sb.toString(); + } +} diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/AuxStatement.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/AuxStatement.java new file mode 100644 index 00000000000..acb7d5158aa --- /dev/null +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/AuxStatement.java @@ -0,0 +1,15 @@ +package de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability; + +import java.util.ArrayList; +import java.util.List; + +import de.uni_freiburg.informatik.ultimate.boogie.BoogieLocation; +import de.uni_freiburg.informatik.ultimate.boogie.ast.Statement; +import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.AuxStatementContainer.StRecExpr; + +public interface AuxStatement { + +public Statement getStatement(StRecExpr stRecExpr); +public BoogieLocation setBoogieLocation(BoogieLocation loc); +public BoogieLocation getBoogieLocation(); +} diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/AuxStatementContainer.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/AuxStatementContainer.java new file mode 100644 index 00000000000..da31df7392c --- /dev/null +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/AuxStatementContainer.java @@ -0,0 +1,88 @@ +package de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability; + +import java.util.ArrayList; +import java.util.HashMap; +import java.util.HashSet; +import java.util.List; +import java.util.Map; +import java.util.Set; + +import de.uni_freiburg.informatik.ultimate.boogie.BoogieLocation; +import de.uni_freiburg.informatik.ultimate.boogie.ast.Statement; +import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.AuxStatementContainer.StRecExpr; + +public class AuxStatementContainer { + public enum StRecExpr { + DECL_VAR, ASSIGN_VAR, IF_ST; + } + + private Map sreMap; + private Set statements; + + public AuxStatementContainer() { + sreMap = new HashMap<>(); + } + + public AuxStatementContainer(AuxStatementContainer auxStatement) { + sreMap = auxStatement.getSreMap(); + } + + public List getStatements(StRecExpr stRecExpr) { + List statList = new ArrayList<>(); + for(AuxStatement auxStatement : sreMap.values()) { + Statement s = auxStatement.getStatement(stRecExpr); + if(s != null) { + statList.add(s); + } + } + return statList; + } + + public Set getRelatedVariableForInstance(Object object) { + Set relatedVariables = new HashSet<>(); + for(Map.Entry entry : sreMap.entrySet()) { + if(entry.getValue().getClass().getName().equals(object.getClass().getName())) { + relatedVariables.add(entry.getKey()); + } + } + return relatedVariables; + } + + public Set setBoogieLocationForInstance(Object object, StRecExpr stRecExpr, final BoogieLocation bl) { + Set statements = new HashSet<>(); + for(Map.Entry entry : sreMap.entrySet()) { + if(entry.getValue().getClass().getName().equals(object.getClass().getName())) { + Statement statement = entry.getValue().getStatement(stRecExpr); + if(statement != null) { + statement.setLoc(bl); + } + statements.add(statement); + } + } + return statements; + } + + public AuxStatement addAuxStatement(String variable, AuxStatement auxStatement) { + if(sreMap == null) { + sreMap = new HashMap<>(); + } + sreMap.put(variable, auxStatement); + return auxStatement; + } + + public Map getSreMap() { + return sreMap; + } + + public void setSreMap(Map sreMap) { + this.sreMap = sreMap; + } + + public Set getStatements() { + return statements; + } + + public void setStatements(Set statements) { + this.statements = statements; + } +} diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/PeaPhaseProgramCounter.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/PeaPhaseProgramCounter.java new file mode 100644 index 00000000000..364e035708d --- /dev/null +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/PeaPhaseProgramCounter.java @@ -0,0 +1,59 @@ +package de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability; + +import java.util.Collection; +import java.util.Iterator; +import java.util.Map; +import java.util.Set; + +import de.uni_freiburg.informatik.ultimate.lib.pea.Phase; +import de.uni_freiburg.informatik.ultimate.lib.pea.PhaseEventAutomata; +import de.uni_freiburg.informatik.ultimate.lib.srparse.pattern.PatternType; + +public class PeaPhaseProgramCounter { + + private final int pc; + private final Phase phase; + private final PhaseEventAutomata pea; + private final PatternType req; + + public PeaPhaseProgramCounter(int pc, Phase phase, PhaseEventAutomata pea, PatternType req) { + super(); + this.pc = pc; + this.phase = phase; + this.pea = pea; + this.req = req; + } + + @Override + public int hashCode() { + return phase.getName().hashCode(); + } + + @Override + public boolean equals(Object o) { + if(this == o) { + return true; + } + if(o instanceof Phase) { + Phase oPhase = (Phase) o; + return phase.getName().equals(oPhase.getName()); + } + return false; + } + + public int getPc() { + return pc; + } + + public Phase getPhase() { + return phase; + } + + public PhaseEventAutomata getPea() { + return pea; + } + + public PatternType getReq() { + return req; + } +} diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/StateRecoverabilityAuxStatement.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/StateRecoverabilityAuxStatement.java new file mode 100644 index 00000000000..c443bb8e051 --- /dev/null +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/StateRecoverabilityAuxStatement.java @@ -0,0 +1,124 @@ +package de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability; + +import java.util.ArrayList; +import java.util.List; + +import de.uni_freiburg.informatik.ultimate.boogie.BoogieLocation; +import de.uni_freiburg.informatik.ultimate.boogie.ast.Statement; +import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.AuxStatementContainer.StRecExpr; + +public class StateRecoverabilityAuxStatement implements AuxStatement { + + private PeaPhaseProgramCounter peaPhasePc; + private String relatedVariable; + private BoogieLocation loc; + private String pcVariable; + private int pc; + private VerificationExpression verificationExpression; + private Statement declVar; + private Statement assignVar; + private Statement ifSt; + + public StateRecoverabilityAuxStatement(String variable) { + this.relatedVariable = variable; + } + + public StateRecoverabilityAuxStatement(PeaPhaseProgramCounter peaPhasePc, String variable, String pcVariable, int pc, VerificationExpression ve) { + this.peaPhasePc = peaPhasePc; + this.relatedVariable = variable; + this.pcVariable = pcVariable; + this.pc = pc; + this.verificationExpression = ve; + } + + @Override + public Statement getStatement(StRecExpr stRecExpr) { + Statement s = null; + switch (stRecExpr) { + case DECL_VAR: + return this.getDeclVar(); + case ASSIGN_VAR: + return this.getAssignVar(); + case IF_ST: + return this.getIfSt(); + default: + break; + } + return null; + } + + public String getRelatedVariable() { + return relatedVariable; + } + + public void setRelatedVariable(String relatedVariable) { + this.relatedVariable = relatedVariable; + } + + public String getPcVariable() { + return pcVariable; + } + + public void setPcVariable(String pcVariable) { + this.pcVariable = pcVariable; + } + + public int getPc() { + return pc; + } + + public void setPc(int pc) { + this.pc = pc; + } + + public VerificationExpression getVerificationExpression() { + return verificationExpression; + } + + public void setVerificationExpression(VerificationExpression verificationExpression) { + this.verificationExpression = verificationExpression; + } + + public Statement getDeclVar() { + return declVar; + } + + public void setDeclVar(Statement declVar) { + this.declVar = declVar; + } + + public Statement getAssignVar() { + return assignVar; + } + + public void setAssignVar(Statement assignVar) { + this.assignVar = assignVar; + } + + public Statement getIfSt() { + return ifSt; + } + + public void setIfSt(Statement ifSt) { + this.ifSt = ifSt; + } + + public PeaPhaseProgramCounter getPeaPhasePc() { + return peaPhasePc; + } + + public void setPeaPhasePc(PeaPhaseProgramCounter peaPhasePc) { + this.peaPhasePc = peaPhasePc; + } + + @Override + public BoogieLocation setBoogieLocation(BoogieLocation loc) { + this.loc = loc; + return loc; + } + + @Override + public BoogieLocation getBoogieLocation() { + return this.loc; + } +} diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/StateRecoverabilityGenerator.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/StateRecoverabilityGenerator.java new file mode 100644 index 00000000000..7d66c870c3c --- /dev/null +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/StateRecoverabilityGenerator.java @@ -0,0 +1,392 @@ +package de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability; + +import java.util.ArrayList; +import java.util.HashMap; +import java.util.HashSet; +import java.util.List; +import java.util.Map; +import java.util.Map.Entry; +import java.util.function.UnaryOperator; +import java.util.stream.Collector; +import java.util.stream.Collectors; +import java.util.Set; + +import javax.management.RuntimeErrorException; + +import de.uni_freiburg.informatik.ultimate.boogie.DeclarationInformation; +import de.uni_freiburg.informatik.ultimate.boogie.ExpressionFactory; +import de.uni_freiburg.informatik.ultimate.boogie.ast.AssignmentStatement; +import de.uni_freiburg.informatik.ultimate.boogie.ast.BinaryExpression; +import de.uni_freiburg.informatik.ultimate.boogie.ast.BinaryExpression.Operator; +import de.uni_freiburg.informatik.ultimate.boogie.ast.Expression; +import de.uni_freiburg.informatik.ultimate.boogie.ast.IdentifierExpression; +import de.uni_freiburg.informatik.ultimate.boogie.ast.IntegerLiteral; +import de.uni_freiburg.informatik.ultimate.boogie.type.BoogieType; +import de.uni_freiburg.informatik.ultimate.core.lib.models.annotation.DefaultLocation; +import de.uni_freiburg.informatik.ultimate.core.model.models.ILocation; +import de.uni_freiburg.informatik.ultimate.core.model.services.ILogger; +import de.uni_freiburg.informatik.ultimate.core.model.services.IUltimateServiceProvider; +import de.uni_freiburg.informatik.ultimate.core.model.services.ILogger.LogLevel; +import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.boogie.Boogie2SMT; +import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.boogie.BoogieDeclarations; +import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.variables.IProgramNonOldVar; +import de.uni_freiburg.informatik.ultimate.lib.pea.BoogieBooleanExpressionDecision; +import de.uni_freiburg.informatik.ultimate.lib.pea.CDD; +import de.uni_freiburg.informatik.ultimate.lib.pea.CounterTrace; +import de.uni_freiburg.informatik.ultimate.lib.pea.Phase; +import de.uni_freiburg.informatik.ultimate.lib.pea.PhaseEventAutomata; +import de.uni_freiburg.informatik.ultimate.lib.pea.Transition; +import de.uni_freiburg.informatik.ultimate.lib.smtlibutils.ManagedScript; +import de.uni_freiburg.informatik.ultimate.lib.smtlibutils.SmtSortUtils; +import de.uni_freiburg.informatik.ultimate.lib.smtlibutils.SmtUtils; +import de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher; +import de.uni_freiburg.informatik.ultimate.lib.smtlibutils.solverbuilder.SolverBuilder; +import de.uni_freiburg.informatik.ultimate.lib.smtlibutils.solverbuilder.SolverBuilder.ExternalSolver; +import de.uni_freiburg.informatik.ultimate.lib.smtlibutils.solverbuilder.SolverBuilder.SolverMode; +import de.uni_freiburg.informatik.ultimate.lib.smtlibutils.solverbuilder.SolverBuilder.SolverSettings; +import de.uni_freiburg.informatik.ultimate.lib.srparse.Durations; +import de.uni_freiburg.informatik.ultimate.lib.srparse.pattern.PatternType; +import de.uni_freiburg.informatik.ultimate.lib.srparse.pattern.PatternType.ReqPeas; +import de.uni_freiburg.informatik.ultimate.logic.Logics; +import de.uni_freiburg.informatik.ultimate.logic.Script; +import de.uni_freiburg.informatik.ultimate.logic.Sort; +import de.uni_freiburg.informatik.ultimate.logic.Script.LBool; +import de.uni_freiburg.informatik.ultimate.logic.Term; +import de.uni_freiburg.informatik.ultimate.logic.TermVariable; +import de.uni_freiburg.informatik.ultimate.pea2boogie.CddToSmt; +import de.uni_freiburg.informatik.ultimate.pea2boogie.IReqSymbolTable; +import de.uni_freiburg.informatik.ultimate.pea2boogie.PeaResultUtil; +import de.uni_freiburg.informatik.ultimate.pea2boogie.generator.RtInconcistencyConditionGenerator; +import de.uni_freiburg.informatik.ultimate.smtinterpol.DefaultLogger; +import de.uni_freiburg.informatik.ultimate.smtinterpol.option.OptionMap; +import de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTInterpol; +import de.uni_freiburg.informatik.ultimate.util.ConstructionCache; + +public class StateRecoverabilityGenerator { + + private IReqSymbolTable mReqSymboltable; + private Term mPrimedInvariant; + private Script mScript; + private ManagedScript mManagedScript; + private Boogie2SMT mBoogie2Smt; + private Map mVars; + private IUltimateServiceProvider mServices; + private ILogger mLogger; + private CddToSmt mCddToSmt; + private PeaResultUtil mPeaResultUtil; + private BoogieDeclarations boogieDeclarations; + + private ConstructionCache mPossibleStartLocations; + + public StateRecoverabilityGenerator( ) { + } + + public StateRecoverabilityGenerator(final ILogger logger, final IUltimateServiceProvider services, final IReqSymbolTable symboltable) { + mReqSymboltable = symboltable; + mServices = services; + mLogger = logger; + + mPeaResultUtil = new PeaResultUtil(mLogger, mServices); + mScript = buildSolver(services); + mManagedScript = new ManagedScript(services, mScript); + + boogieDeclarations = new BoogieDeclarations(mReqSymboltable.getDeclarations(), mLogger); + mBoogie2Smt = new Boogie2SMT(mManagedScript, boogieDeclarations, services, false); + mVars = mBoogie2Smt.getBoogie2SmtSymbolTable().getGlobalsMap(); + + mPossibleStartLocations = new ConstructionCache<>(this::constructSearchStartLocationTerm); + mCddToSmt = new CddToSmt(mServices, mPeaResultUtil, mScript, mBoogie2Smt, boogieDeclarations, mReqSymboltable); + } + + public Map> getRelevantLocationsFromPea(List reqPeasList, VerificationExpressionContainer vec) { + Map> veLocation = new HashMap<>(); + Set reqPeasSet = new HashSet<>(reqPeasList); + Set declaredConstants = new HashSet<>(); + Map reqPeasTerm = new HashMap<>(); + + // Create Terms for every location + for(ReqPeas reqPeas : reqPeasList) { + List> ctPeaList = reqPeas.getCounterTrace2Pea(); + Term parallelAutomaton = generateParallelAutomatonTerm(removeReqPeas(reqPeasSet, reqPeas)); + reqPeasTerm.put(reqPeas, parallelAutomaton); + } + + for(ReqPeas reqPea : reqPeasList) { + List> ctPeaList = reqPea.getCounterTrace2Pea(); + PatternType req = reqPea.getPattern(); + for(Entry entry : ctPeaList) { + Phase[] phases = entry.getValue().getPhases(); + for(int i = 0; i < phases.length; ++i) { + Phase phase = phases[i]; + // Check for every phase if the location can fulfill the verification expression + // TRUE -> Do not add the phase + // FALSE -> Add the phase + for(VerificationExpression ve : vec.getVerificationExpressions().values()) { + CDD veCcd = BoogieBooleanExpressionDecision.create(createOppositeCondition(new DefaultLocation(), ve.getBoogiePrimitiveType(), ve.getVariable(), ve.getOperator(), ve.getValue())); + List invariantVeList = new ArrayList<>(); + + // Compute phase invariant ⋀ opposite verification expression + final Term termVe = mCddToSmt.toSmt(veCcd); + invariantVeList.add(termVe); + final Term termLocation = mCddToSmt.toSmt(phase.getStateInvariant()); + invariantVeList.add(termLocation); + + //Find satisfiable model + final Term termModel = SmtUtils.and(mScript, invariantVeList); + + if(SmtUtils.checkSatTerm(mScript, termModel) == LBool.SAT) { + if(!veLocation.containsKey(ve)) { + veLocation.put(ve, new HashSet<>()); + } + + Term possibleStartPhase = possibleStartPhase(phase, reqPea, reqPeasTerm.get(reqPea), termVe); + + // Declare constants for Z3 + declareConstants(mScript, possibleStartPhase, declaredConstants); + + if(SmtUtils.checkSatTerm(mScript, possibleStartPhase) == LBool.SAT) { + veLocation.get(ve).add(new PeaPhaseProgramCounter(i, phase, entry.getValue(), req)); + } + } + } + } + } + } + return veLocation; + } + + private void declareConstants(Script script, Term term, Set declaredConstants) { + Sort sort = term.getSort(); + TermVariable[] termVariables = term.getFreeVars(); + for(int i = 0; i < termVariables.length; ++i) { + //mScript.declareFun("ENG_READY", new Sort[0], sort); + TermVariable termVariable = termVariables[i]; + if(!declaredConstants.contains(termVariable.getName())) { + script.declareFun(termVariable.getName(), new Sort[0], sort); + declaredConstants.add(termVariable.getName()); + } + } + } + + private Term possibleStartPhase(Phase phase, ReqPeas reqPeas, Term parallelAutomaton, Term termVe) { + Term actualTerm = generatePhaseTerm(phase); + Term[] terms = new Term[] {actualTerm, parallelAutomaton, termVe}; + + final Term finalTerm = termAnd(terms); + return finalTerm; + } + + private Term termAnd(Term[] terms) { + final Term term = SmtUtils.and(mScript, terms); + return term; + } + + private Term generatePhaseTerm(Phase phase) { + final Term term = mCddToSmt.toSmt(phase.getStateInvariant()); + return term; + } + + private Set removeReqPeas(Set reqPeasSet, ReqPeas reqPeas) { + Set newReqPeasSet = new HashSet<>(reqPeasSet); + newReqPeasSet.remove(reqPeas); + return newReqPeasSet; + } + + /** + * Computes VE && (A_1 && A_2 && A_n && ...) + * + * A = ((p_1 && (g_1 || g_n)) || (p_2 && (g_n)) || ...) + * @param reqPeas + * @return term + */ + private Term generateParallelAutomatonTerm(Set reqPeas) { + Map reqPeasPeaArrayMap = createPeaArray(reqPeas); + CDD reqsCDD = null; + for(Map.Entry entry : reqPeasPeaArrayMap.entrySet()) { + + // Automatons per requirement + CDD peasCDD = null; + PhaseEventAutomata[] peaArray = entry.getValue(); + for(PhaseEventAutomata pea : peaArray) { + Phase[] phases = pea.getPhases(); + + // Create CDD for every location and guard + CDD[] invariantPhaseGuardArrayPerPea = new CDD[pea.getPhases().length]; + for(int i = 0; i < invariantPhaseGuardArrayPerPea.length; ++i) { + Phase phase = phases[i]; + CDD invariantPhaseGuardCDD = phase.getStateInvariant().and(phase.getClockInvariant()); + invariantPhaseGuardArrayPerPea[i] = invariantPhaseGuardCDD; + } + + // Link every location-guard CDD with OR + CDD peaCDD = null; + for(int i = 0; i < invariantPhaseGuardArrayPerPea.length; ++i) { + if(peaCDD == null) { + peaCDD = invariantPhaseGuardArrayPerPea[i]; + } + peaCDD.or(invariantPhaseGuardArrayPerPea[i]); + } + + // Link every pea with AND + if(peasCDD == null) { + peasCDD = peaCDD; + } else { + peasCDD.and(peaCDD); + } + } + // Link every req with AND + if(reqsCDD == null) { + reqsCDD = peasCDD; + } else { + reqsCDD.and(peasCDD); + } + } + final Term term = mCddToSmt.toSmt(reqsCDD); + return term; + } + private Map createPeaArray(Set reqPeas) { + Map reqPeasPeaArrayMap = new HashMap<>(); + for(ReqPeas reqPea : reqPeas) { + List> ctPeaList = reqPea.getCounterTrace2Pea(); + Set automataSet = ctPeaList.stream().map(Entry::getValue).collect(Collectors.toSet()); + final PhaseEventAutomata[] automata = automataSet.toArray(new PhaseEventAutomata[automataSet.size()]); + reqPeasPeaArrayMap.put(reqPea, automata); + } + return reqPeasPeaArrayMap; + } + + private Term constructSearchStartLocationTerm(Phase phase) { + return transformAndLog(phase.getStateInvariant(), "phase invariant"); + } + + private Term transformAndLog(final CDD org, final String msg) { + final Term term = mCddToSmt.toSmt(org); + mLogger.info("Can be start location %s %s", msg, org.toGeneralString()); + return term; + } + + private static Script buildSolver(final IUltimateServiceProvider services) throws AssertionError { + SolverSettings settings = SolverBuilder.constructSolverSettings() + //.setSolverMode(SolverMode.External_ModelsAndUnsatCoreMode).setUseExternalSolver(ExternalSolver.Z3); + .setSolverMode(SolverMode.External_ModelsMode).setUseExternalSolver(ExternalSolver.Z3); + return SolverBuilder.buildAndInitializeSolver(services, settings, "RtInconsistencySolver"); + } + + public Map>> getAuxStatementPerVerificationExpression(AuxStatementContainer auxStatementContainer) { + Map>> vePeaAuxStatementMap = new HashMap<>(); + for(AuxStatement auxStatement : auxStatementContainer.getSreMap().values()) { + if(auxStatement instanceof StateRecoverabilityAuxStatement) { + StateRecoverabilityAuxStatement stRecAuxSt = (StateRecoverabilityAuxStatement) auxStatement; + if(!vePeaAuxStatementMap.containsKey(stRecAuxSt.getVerificationExpression())) { + vePeaAuxStatementMap.put(stRecAuxSt.getVerificationExpression(), new HashMap<>()); + } + Map> peaAuxStatementMap = vePeaAuxStatementMap.get(stRecAuxSt.getVerificationExpression()); + if(!peaAuxStatementMap.containsKey(stRecAuxSt.getPeaPhasePc().getPea())) { + peaAuxStatementMap.put(stRecAuxSt.getPeaPhasePc().getPea(), new HashSet<>()); + } + Set stRecAuxStSet = peaAuxStatementMap.get(stRecAuxSt.getPeaPhasePc().getPea()); + stRecAuxStSet.add(stRecAuxSt); + } + } + return vePeaAuxStatementMap; + } + + public Expression createOppositeCondition(final ILocation loc, BoogieType boogieType, String lhs, String opr, String rhs) { + String newOpr = ""; + switch (opr) { + case "==": + newOpr = "!="; + break; + case "!=": + newOpr = "=="; + break; + case "<": + newOpr = ">="; + break; + case ">": + newOpr = "<="; + break; + case "<=": + newOpr = ">"; + break; + case ">=": + newOpr = "<"; + break; + default: + throw new RuntimeException(getClass().getName() + "Could not parse token: " + opr); + } + return createExpression(loc, boogieType, lhs, newOpr, rhs); + } + + public Expression createExpression(final ILocation loc, BoogieType boogieType, String sLhs, Operator opr, String sRhs) { + Expression rhs = null; + Expression lhs; + lhs = new IdentifierExpression(loc, boogieType, sLhs, DeclarationInformation.DECLARATIONINFO_GLOBAL); + switch (boogieType.toString()) { + case "int": + rhs = ExpressionFactory.createIntegerLiteral(loc, sRhs); + break; + case "bool": + boolean bValue = "true".equalsIgnoreCase(sRhs) ? true : false; + rhs = ExpressionFactory.createBooleanLiteral(loc, bValue); + break; + case "real": + rhs = ExpressionFactory.createRealLiteral(loc, sRhs); + break; + case "type-error": + throw new RuntimeErrorException(null, getClass().getName() + ": " + boogieType + " no known data type."); + } + Expression expression = ExpressionFactory.newBinaryExpression(loc, opr, lhs, rhs); + return expression; + } + + public Expression createExpression(final ILocation loc, BoogieType boogieType, String sLhs, String sOpr, String sRhs) { + Expression rhs = null; + Expression lhs; + BinaryExpression.Operator opr; + lhs = new IdentifierExpression(loc, boogieType, sLhs, DeclarationInformation.DECLARATIONINFO_GLOBAL); + switch (boogieType.toString()) { + case "int": + rhs = ExpressionFactory.createIntegerLiteral(loc, sRhs); + break; + case "bool": + boolean bValue = "true".equalsIgnoreCase(sRhs) ? true : false; + rhs = ExpressionFactory.createBooleanLiteral(loc, bValue); + break; + case "real": + rhs = ExpressionFactory.createRealLiteral(loc, sRhs); + break; + case "type-error": + throw new RuntimeErrorException(null, getClass().getName() + ": " + boogieType + " no known data type."); + } + opr = getOperator(sOpr); + Expression expression = ExpressionFactory.newBinaryExpression(loc, opr, lhs, rhs); + return expression; + } + + private BinaryExpression.Operator getOperator(String sOpr) { + switch (sOpr) { + case "||": + case "|": + return Operator.LOGICOR; + case "&&": + case "&": + return Operator.LOGICAND; + case "==": + return Operator.COMPEQ; + case "!=": + return Operator.COMPNEQ; + case "<": + return Operator.COMPLT; + case ">": + return Operator.COMPGT; + case "<=": + return Operator.COMPLEQ; + case ">=": + return Operator.COMPGEQ; + default: + throw new RuntimeErrorException(null, getClass().getName() + ": Could not parse operator."); + } + } +} + diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/VerificationExpression.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/VerificationExpression.java new file mode 100644 index 00000000000..6c169a80876 --- /dev/null +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/VerificationExpression.java @@ -0,0 +1,74 @@ +package de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability; + +import javax.management.RuntimeErrorException; + +import de.uni_freiburg.informatik.ultimate.boogie.type.BoogiePrimitiveType; + +public class VerificationExpression { + private final String[] expr; + private final String dataType; + private final int iVariable = 0; + private final int iOperator = 1; + private final int iValue = 2; + + public VerificationExpression(String[] expr, String dataType) { + this.expr = expr; + this.dataType = dataType; + } + public String[] getExpr() { + return expr; + } + + public String getVariable() { + return expr[iVariable]; + } + + public String getOperator() { + return expr[iOperator]; + } + + public String getValue() { + return expr[iValue]; + } + + public String getDataType( ) { + return dataType; + } + + public boolean getBoolValue() { + if(expr[iValue].equals(VerificationExpressionContainer.BOOL)) { + return Boolean.getBoolean(expr[iValue]); + } + + throw new RuntimeErrorException(null, getClass().getName() + " data type " + dataType + " is not correct for " + expr); + } + + public int getIntegerValue() { + if(expr[iValue].equals(VerificationExpressionContainer.INT)) { + return Integer.getInteger(expr[iValue]); + } + + throw new RuntimeErrorException(null, getClass().getName() + " data type " + dataType + " is not correct for " + expr); + } + + public double getDoubleValue() { + if(expr[iValue].equals(VerificationExpressionContainer.REAL)) { + return Double.parseDouble(expr[iValue]); + } + + throw new RuntimeErrorException(null, getClass().getName() + " data type " + dataType + " is not correct for " + expr); + } + + public BoogiePrimitiveType getBoogiePrimitiveType() { + switch (dataType) { + case "bool": + return BoogiePrimitiveType.TYPE_BOOL; + case "int": + return BoogiePrimitiveType.TYPE_INT; + case "real": + return BoogiePrimitiveType.TYPE_REAL; + default: + return BoogiePrimitiveType.TYPE_ERROR; + } + } +} diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/VerificationExpressionContainer.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/VerificationExpressionContainer.java new file mode 100644 index 00000000000..cc56e47c060 --- /dev/null +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/VerificationExpressionContainer.java @@ -0,0 +1,97 @@ +package de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability; + +import java.util.ArrayList; +import java.util.HashMap; +import java.util.List; +import java.util.Map; +import java.util.Map.Entry; +import java.util.regex.Matcher; +import java.util.regex.Pattern; + +import javax.management.RuntimeErrorException; + +import de.uni_freiburg.informatik.ultimate.lib.pea.CounterTrace; +import de.uni_freiburg.informatik.ultimate.lib.pea.PhaseEventAutomata; +import de.uni_freiburg.informatik.ultimate.lib.srparse.pattern.PatternType.ReqPeas; +import de.uni_freiburg.informatik.ultimate.pea2boogie.req2pea.IReq2Pea; + +public class VerificationExpressionContainer { + + //Pattern for input expression + public static final String exprPattern = "\\s{0,1}((\\w+)\\s*([<>=!][=]*)\\s*(\\w+))\\s{0,1}"; + + //Data types + public static final String BOOL = "bool"; + public static final String INT = "int"; + public static final String REAL = "real"; + + private IReq2Pea mReq2pea; + private Map mVerificationExpressions; + private Map mVariableDataTypeMap; + + public VerificationExpressionContainer(IReq2Pea req2pea) { + mReq2pea = req2pea; + mVerificationExpressions = new HashMap<>(); + getDataTypeFromReq2Pea(req2pea); + } + + private void getDataTypeFromReq2Pea(IReq2Pea req2Pea) { + Map variableDataTypeMap = new HashMap<>(); + for(ReqPeas reqPeas : req2Pea.getReqPeas()) { + List> mReq = reqPeas.getCounterTrace2Pea(); + for(Entry entry : mReq) { + PhaseEventAutomata pea = entry.getValue(); + for(Map.Entry entryVariableDataType : pea.getVariables().entrySet()) { + //TODO anpassen abhängig davon was es noch für Datentypen gibt + variableDataTypeMap.put(entryVariableDataType.getKey(), entryVariableDataType.getValue()); + } + } + } + mVariableDataTypeMap = variableDataTypeMap; + } + + public Map getVerificationExpressions() { + return mVerificationExpressions; + } + + public void addExpression(String inputExpr) { + List veList = new ArrayList<>(); + int grpVariable = 2; + int grpOperator = 3; + int grpValue = 4; + String[] exprArray = inputExpr.split(","); + for(String expr : exprArray) { + Matcher m = match(expr, exprPattern); + if(m.find()) { + String sVariable = m.group(grpVariable); + String sOperator = m.group(grpOperator); + String sValue = m.group(grpValue); + String dataType = mVariableDataTypeMap.get(sVariable); + if(dataType == null) { + throw new IllegalArgumentException(getClass().getName() + " could not find data type for " + sVariable); + } + veList.add(new VerificationExpression(new String[] {sVariable, sOperator, sValue}, dataType)); + } + } + addVerificationExpression(veList); + } + + private void addVerificationExpression(List veList) { + for(VerificationExpression ve : veList) { + addVerificationExpression(ve); + } + } + + private void addVerificationExpression(VerificationExpression ve) { + if(mVerificationExpressions == null) { + mVerificationExpressions = new HashMap<>(); + } + mVerificationExpressions.put(ve.getVariable(), ve); + } + + private Matcher match(String s, String pattern) { + Pattern p = Pattern.compile(pattern); + Matcher m = p.matcher(s); + return m; + } +} diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/testgen/Req2CauseTrackingPea.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/testgen/Req2CauseTrackingPea.java index a24805dc9aa..e8e4b1a1379 100644 --- a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/testgen/Req2CauseTrackingPea.java +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/testgen/Req2CauseTrackingPea.java @@ -96,7 +96,7 @@ public void transform(final IReq2Pea req2pea) { builder.addInitPattern(p); mDurations.addInitPattern(p); if (p.getCategory() == VariableCategory.OUT) { - builder.addAuxvar(ReqTestAnnotator.getTrackingVar(p.getId()), "bool", p); + builder.addAuxVarPrimedAndUnprimed(ReqTestAnnotator.getTrackingVar(p.getId()), "bool", p); } } for (final ReqPeas reqpea : simplePeas) { diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/testgen/Req2ModifySymbolTablePea.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/testgen/Req2ModifySymbolTablePea.java new file mode 100644 index 00000000000..a10ddc5172f --- /dev/null +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/testgen/Req2ModifySymbolTablePea.java @@ -0,0 +1,246 @@ +package de.uni_freiburg.informatik.ultimate.pea2boogie.testgen; + +import java.util.ArrayList; +import java.util.HashMap; +import java.util.Iterator; +import java.util.List; +import java.util.Map; +import java.util.Map.Entry; +import java.util.Set; +import java.util.regex.Matcher; +import java.util.regex.Pattern; + +import de.uni_freiburg.informatik.ultimate.boogie.DeclarationInformation; +import de.uni_freiburg.informatik.ultimate.boogie.DeclarationInformation.StorageClass; +import de.uni_freiburg.informatik.ultimate.boogie.ExpressionFactory; +import de.uni_freiburg.informatik.ultimate.boogie.ast.AssignmentStatement; +import de.uni_freiburg.informatik.ultimate.boogie.ast.BinaryExpression; +import de.uni_freiburg.informatik.ultimate.boogie.ast.BooleanLiteral; +import de.uni_freiburg.informatik.ultimate.boogie.ast.Expression; +import de.uni_freiburg.informatik.ultimate.boogie.ast.IdentifierExpression; +import de.uni_freiburg.informatik.ultimate.boogie.ast.IfStatement; +import de.uni_freiburg.informatik.ultimate.boogie.ast.IntegerLiteral; +import de.uni_freiburg.informatik.ultimate.boogie.ast.LeftHandSide; +import de.uni_freiburg.informatik.ultimate.boogie.ast.Statement; +import de.uni_freiburg.informatik.ultimate.boogie.ast.VariableLHS; +import de.uni_freiburg.informatik.ultimate.boogie.ast.BinaryExpression.Operator; +import de.uni_freiburg.informatik.ultimate.boogie.type.BoogiePrimitiveType; +import de.uni_freiburg.informatik.ultimate.boogie.type.BoogieType; +import de.uni_freiburg.informatik.ultimate.core.lib.models.annotation.DefaultLocation; +import de.uni_freiburg.informatik.ultimate.core.model.models.IBoogieType; +import de.uni_freiburg.informatik.ultimate.core.model.models.ILocation; +import de.uni_freiburg.informatik.ultimate.core.model.preferences.IPreferenceProvider; +import de.uni_freiburg.informatik.ultimate.core.model.services.ILogger; +import de.uni_freiburg.informatik.ultimate.core.model.services.IUltimateServiceProvider; +import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.boogie.BoogieDeclarations; +import de.uni_freiburg.informatik.ultimate.lib.pea.CounterTrace; +import de.uni_freiburg.informatik.ultimate.lib.pea.Decision; +import de.uni_freiburg.informatik.ultimate.lib.pea.Phase; +import de.uni_freiburg.informatik.ultimate.lib.pea.PhaseEventAutomata; +import de.uni_freiburg.informatik.ultimate.lib.pea.RangeDecision; +import de.uni_freiburg.informatik.ultimate.lib.srparse.Durations; +import de.uni_freiburg.informatik.ultimate.lib.srparse.pattern.DeclarationPattern; +import de.uni_freiburg.informatik.ultimate.lib.srparse.pattern.DeclarationPattern.VariableCategory; +import de.uni_freiburg.informatik.ultimate.lib.srparse.pattern.PatternType; +import de.uni_freiburg.informatik.ultimate.lib.srparse.pattern.PatternType.ReqPeas; +import de.uni_freiburg.informatik.ultimate.pea2boogie.Activator; +import de.uni_freiburg.informatik.ultimate.pea2boogie.IReqSymbolTable; +import de.uni_freiburg.informatik.ultimate.pea2boogie.preferences.Pea2BoogiePreferences; +import de.uni_freiburg.informatik.ultimate.pea2boogie.req2pea.IReq2Pea; +import de.uni_freiburg.informatik.ultimate.pea2boogie.req2pea.IReq2PeaAnnotator; +import de.uni_freiburg.informatik.ultimate.pea2boogie.req2pea.ReqCheckAnnotator; +import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.VerificationExpression; +import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.VerificationExpressionContainer; +import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.AuxStatement; +import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.PeaPhaseProgramCounter; +import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.StateRecoverabilityAuxStatement; +import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.StateRecoverabilityGenerator; +import de.uni_freiburg.informatik.ultimate.pea2boogie.translator.ReqSymboltableBuilder; +import de.uni_freiburg.informatik.ultimate.pea2boogie.translator.ReqSymboltableBuilder.ErrorInfo; +import de.uni_freiburg.informatik.ultimate.pea2boogie.translator.ReqSymboltableBuilder.ErrorType; + +public class Req2ModifySymbolTablePea implements IReq2Pea { + + private final IUltimateServiceProvider mServices; + private final ILogger mLogger; + private final List mInitPattern; + private final List mReqPeas; + private IReqSymbolTable mSymbolTable; + private final Durations mDurations; + private boolean mHasErrors; + private final IPreferenceProvider prefs; + private ILocation loc; + private StateRecoverabilityGenerator stRecGen; + + public Req2ModifySymbolTablePea(final IUltimateServiceProvider services, final ILogger logger, final List init) { + mServices = services; + mLogger = logger; + mInitPattern = init; + mReqPeas = new ArrayList<>(); + mDurations = new Durations(); + prefs = mServices.getPreferenceProvider(Activator.PLUGIN_ID); + } + + @Override + public List getReqPeas() { + return mReqPeas; + } + + @Override + public IReqSymbolTable getSymboltable() { + return mSymbolTable; + } + + @Override + public Durations getDurations() { + return mDurations; + } + + @Override + public void transform(IReq2Pea req2pea) { + final VerificationExpressionContainer vec = getVerificationExpression(req2pea); + + final List simplePeas = req2pea.getReqPeas(); + final IReqSymbolTable oldSymbolTable = req2pea.getSymboltable(); + stRecGen = new StateRecoverabilityGenerator(mLogger, mServices, oldSymbolTable); + final ReqSymboltableBuilder builder = new ReqSymboltableBuilder(mLogger, oldSymbolTable); + + //Passing the variable definitions + for (final DeclarationPattern p : mInitPattern) { + builder.addInitPattern(p); + mDurations.addInitPattern(p); + } + + //Übergabe der PEAs + for (final ReqPeas reqpea : simplePeas) { + mReqPeas.add(reqpea); + final PatternType pattern = reqpea.getPattern(); + mDurations.addNonInitPattern(pattern); + for (final Entry pea : reqpea.getCounterTrace2Pea()) { + builder.addPea(reqpea.getPattern(), pea.getValue()); + } + } + + //Collecting the PEAs and ProgramCounter + //Necessary in Transformer since otherwise unused global variables would be in the Boogie code + Map> veLocationMap = stRecGen.getRelevantLocationsFromPea(simplePeas, vec); + + List sreList = createGlobalVariableForVerificationExpression(builder, veLocationMap, vec); + + //Creating the statements + createAssignBoolToGlobalVariableBeforeWhileLoop(sreList); + createIfStatementInWhileLoop(sreList); + + mSymbolTable = builder.constructSymbolTable(); + } + + private void createIfStatementInWhileLoop(List auxStatements) { + for(AuxStatement auxStatement : auxStatements) { + if(auxStatement instanceof StateRecoverabilityAuxStatement) { + StateRecoverabilityAuxStatement auxStatementStRec = (StateRecoverabilityAuxStatement) auxStatement; + VerificationExpression ve = auxStatementStRec.getVerificationExpression(); + ILocation loc = auxStatementStRec.getBoogieLocation(); + // Create expression + //Opposite of verification Expression + Expression condition1 = stRecGen.createOppositeCondition(loc, BoogiePrimitiveType.toPrimitiveType(ve.getDataType()), ve.getVariable(), ve.getOperator(), ve.getValue()); + // Program counter state + Expression condition2 = stRecGen.createExpression(loc, BoogieType.TYPE_INT, auxStatementStRec.getPcVariable(), Operator.COMPEQ, String.valueOf(auxStatementStRec.getPc())); + Expression condition1And2 = ExpressionFactory.newBinaryExpression(loc, Operator.LOGICAND, condition1, condition2); + BooleanLiteral booleanLiteral = ExpressionFactory.createBooleanLiteral(loc, true); + // Create assignment + AssignmentStatement assignmentStatement = genAssignmentStmt(loc, auxStatementStRec.getRelatedVariable(), booleanLiteral); + IfStatement ifStatement = new IfStatement(loc, condition1And2, new Statement[] {assignmentStatement}, new Statement[0]); + auxStatementStRec.setIfSt(ifStatement); + } + } + } + + private VerificationExpressionContainer getVerificationExpression(IReq2Pea req2pea) { + final VerificationExpressionContainer vec = new VerificationExpressionContainer(req2pea); + //Gets verification expression from GUI + String verExpr = prefs.getString(Pea2BoogiePreferences.LABEL_STATE_RECOVERABILITY_VER_EXPR); + vec.addExpression(verExpr); + return vec; + } + + private List createGlobalVariableForVerificationExpression(ReqSymboltableBuilder builder, Map> veLocationMaptionMap, VerificationExpressionContainer vec) { + List sreList = new ArrayList<>(); + for(Map.Entry> entry : veLocationMaptionMap.entrySet()) { + for(PeaPhaseProgramCounter peaPhasePc : entry.getValue()) { + String pcName = getPcName(peaPhasePc.getPea().getName()); + int pc = peaPhasePc.getPc(); + //Erstelle für jede angegebene Bedingung eine globale Variable für alle PCs + String variable = entry.getKey().getVariable(); + String dataType = entry.getKey().getDataType(); + String globalVariable = pcName + pc + "_StRec_" + variable; + StateRecoverabilityAuxStatement auxStatement = new StateRecoverabilityAuxStatement(peaPhasePc, globalVariable, pcName, pc, entry.getKey()); + sreList.add(builder.addAuxVar(auxStatement, globalVariable, "bool", null)); + } + + } + return sreList; + } + + private void createAssignBoolToGlobalVariableBeforeWhileLoop(List auxStatements) { + for(AuxStatement auxStatement : auxStatements) { + if(auxStatement instanceof StateRecoverabilityAuxStatement) { + StateRecoverabilityAuxStatement auxStatementStateRecoverability = (StateRecoverabilityAuxStatement) auxStatement; + BooleanLiteral booleanLiteral = ExpressionFactory.createBooleanLiteral(null, false); + AssignmentStatement assignmentStatement = genAssignmentStmt(constructNewLocation(), auxStatementStateRecoverability.getRelatedVariable(), booleanLiteral); + auxStatementStateRecoverability.setAssignVar(assignmentStatement); + } + } + } + + private String getPcName(String s) { + //Decision decision = phase.getClockInvariant().getDecision(); + //if(decision != null) { + // return decision.getVar(); + //} + return s + "_pc"; + } + + private Matcher match(String text, String pattern) { + Pattern p = Pattern.compile(pattern); + Matcher m = p.matcher(text); + return m; + } + + private static AssignmentStatement genAssignmentStmt(final ILocation bl, final String id, final Expression val) { + return genAssignmentStmt(bl, new VariableLHS(bl, id), val); + } + + private static AssignmentStatement genAssignmentStmt(final ILocation bl, final VariableLHS lhs, + final Expression val) { + assert lhs.getLocation() == bl; + return new AssignmentStatement(bl, new LeftHandSide[] { lhs }, new Expression[] { val }); + } + + private ILocation constructNewLocation() { + return new DefaultLocation(); + } + + private IBoogieType getBoogieType(String type) { + switch (type.toLowerCase()) { + case "bool": + case "real": + case "int": + return BoogiePrimitiveType.toPrimitiveType(type); + case "event": + return BoogieType.TYPE_BOOL; + default: + return BoogieType.TYPE_ERROR; + } + } + + @Override + public boolean hasErrors() { + return mHasErrors; + } + + @Override + public IReq2PeaAnnotator getAnnotator() { + return new ReqCheckAnnotator(mServices, mLogger, getReqPeas(), getSymboltable(), getDurations()); + } + +} diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/testgen/Req2ModifySymbolTablePeaTransformer.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/testgen/Req2ModifySymbolTablePeaTransformer.java new file mode 100644 index 00000000000..66826783d1b --- /dev/null +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/testgen/Req2ModifySymbolTablePeaTransformer.java @@ -0,0 +1,32 @@ +package de.uni_freiburg.informatik.ultimate.pea2boogie.testgen; + +import java.util.List; +import java.util.Map; + +import de.uni_freiburg.informatik.ultimate.core.model.services.ILogger; +import de.uni_freiburg.informatik.ultimate.core.model.services.IUltimateServiceProvider; +import de.uni_freiburg.informatik.ultimate.lib.pea.PhaseEventAutomata; +import de.uni_freiburg.informatik.ultimate.lib.srparse.pattern.DeclarationPattern; +import de.uni_freiburg.informatik.ultimate.lib.srparse.pattern.PatternType; +import de.uni_freiburg.informatik.ultimate.pea2boogie.req2pea.IReq2Pea; +import de.uni_freiburg.informatik.ultimate.pea2boogie.req2pea.IReq2PeaTransformer; + +public class Req2ModifySymbolTablePeaTransformer implements IReq2PeaTransformer { + + private final ILogger mLogger; + private final IUltimateServiceProvider mServices; + + public Req2ModifySymbolTablePeaTransformer(final IUltimateServiceProvider services, final ILogger logger) { + mLogger = logger; + mServices = services; + } + + @Override + public IReq2Pea transform(final IReq2Pea req2pea, final List init, final List> requirements) { + final Req2ModifySymbolTablePea req2ModifySymbolTablePea = new Req2ModifySymbolTablePea(mServices, mLogger, init); + + req2ModifySymbolTablePea.transform(req2pea); + return req2ModifySymbolTablePea; + } + +} diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/translator/Req2BoogieTranslator.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/translator/Req2BoogieTranslator.java index 7259a2dc779..d5aa79102e1 100644 --- a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/translator/Req2BoogieTranslator.java +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/translator/Req2BoogieTranslator.java @@ -84,6 +84,8 @@ import de.uni_freiburg.informatik.ultimate.pea2boogie.req2pea.IReq2PeaAnnotator; import de.uni_freiburg.informatik.ultimate.pea2boogie.req2pea.IReq2PeaTransformer; import de.uni_freiburg.informatik.ultimate.pea2boogie.req2pea.Req2Pea; +import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.StateRecoverabilityAuxStatement; +import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.AuxStatementContainer.StRecExpr; import de.uni_freiburg.informatik.ultimate.pea2boogie.testgen.ReqInOutGuesser; import de.uni_freiburg.informatik.ultimate.util.simplifier.NormalFormTransformer; @@ -557,11 +559,13 @@ private Statement[] genWhileLoopBody(final BoogieLocation bl) { mSymboltable.getPcName(pea.getValue()), bl)); } } - + // Assign St-Recoverability if statement + //stmtList.addAll(mSymboltable.getAuxStatements().setBoogieLocationForInstance(new StateRecoverabilityAuxStatement(""), StRecExpr.IF_ST, bl)); + stmtList.addAll(mSymboltable.getAuxStatementContainer().getStatements(StRecExpr.IF_ST)); stmtList.addAll(mReqCheckAnnotator.getStateChecks()); stmtList.addAll( mSymboltable.getPcVars().stream().map(this::genStateVarAssignHistory).collect(Collectors.toList())); - + for (final ReqPeas reqpea : mReqPeas) { for (final Entry ct2pea : reqpea.getCounterTrace2Pea()) { final PhaseEventAutomata pea = ct2pea.getValue(); @@ -662,6 +666,9 @@ private Statement[] generateProcedureBody(final BoogieLocation bl, final List init) { modifiedVarsList.addAll(mSymboltable.getPrimedVars()); modifiedVarsList.addAll(mSymboltable.getHistoryVars()); modifiedVarsList.addAll(mSymboltable.getEventVars()); + // Adds only instance of class type StateRecoverabilityAuxStatement + modifiedVarsList.addAll(mSymboltable.getAuxStatementContainer().getRelatedVariableForInstance(new StateRecoverabilityAuxStatement(""))); final VariableLHS[] modifiedVars = new VariableLHS[modifiedVarsList.size()]; for (int i = 0; i < modifiedVars.length; i++) { diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/translator/ReqSymboltableBuilder.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/translator/ReqSymboltableBuilder.java index 53f00f8e527..248c1e892c7 100644 --- a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/translator/ReqSymboltableBuilder.java +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/translator/ReqSymboltableBuilder.java @@ -38,6 +38,8 @@ import java.util.Set; import java.util.stream.Collectors; +import org.eclipse.core.runtime.IRegistryChangeEvent; + import de.uni_freiburg.informatik.ultimate.boogie.BoogieLocation; import de.uni_freiburg.informatik.ultimate.boogie.DeclarationInformation; import de.uni_freiburg.informatik.ultimate.boogie.ExpressionFactory; @@ -65,6 +67,8 @@ import de.uni_freiburg.informatik.ultimate.lib.srparse.pattern.DeclarationPattern.VariableCategory; import de.uni_freiburg.informatik.ultimate.lib.srparse.pattern.PatternType; import de.uni_freiburg.informatik.ultimate.pea2boogie.IReqSymbolTable; +import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.AuxStatement; +import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.AuxStatementContainer; import de.uni_freiburg.informatik.ultimate.util.datastructures.UnionFind; import de.uni_freiburg.informatik.ultimate.util.datastructures.relation.LinkedHashRelation; @@ -82,6 +86,9 @@ public class ReqSymboltableBuilder { private final Map mId2Type; private final Map mId2IdExpr; private final Map mId2VarLHS; + + private final AuxStatementContainer mAuxStatements; + private final Set mAuxVars; private final Set mStateVars; private final Set mConstVars; private final Set mPrimedVars; @@ -106,6 +113,8 @@ public ReqSymboltableBuilder(final ILogger logger) { mId2IdExpr = new LinkedHashMap<>(); mId2VarLHS = new LinkedHashMap<>(); + mAuxStatements = new AuxStatementContainer(); + mAuxVars = new LinkedHashSet<>(); mStateVars = new LinkedHashSet<>(); mConstVars = new LinkedHashSet<>(); mPrimedVars = new LinkedHashSet<>(); @@ -122,6 +131,37 @@ public ReqSymboltableBuilder(final ILogger logger) { mBuiltinFunctions = generateBuildinFuntions(); } + + //Copy constructor SymbolTable + + public ReqSymboltableBuilder(ILogger logger, IReqSymbolTable iReqSymbolTable) { + mLogger = logger; + mId2Errors = new LinkedHashRelation<>(); + //mId2Type = new LinkedHashMap<>(iReqSymbolTable.getId2Type()); + //mId2IdExpr = new LinkedHashMap<>(iReqSymbolTable.getId2IdExpr()); + //mId2VarLHS = new LinkedHashMap<>(iReqSymbolTable.getId2VarLHS()); + mId2Type = new LinkedHashMap<>(); + mId2IdExpr = new LinkedHashMap<>(); + mId2VarLHS = new LinkedHashMap<>(); + + mAuxStatements = iReqSymbolTable.getAuxStatementContainer(); + mAuxVars = new LinkedHashSet(iReqSymbolTable.getAuxVars()); + mStateVars = new LinkedHashSet(iReqSymbolTable.getStateVars()); + mConstVars = new LinkedHashSet(iReqSymbolTable.getConstVars()); + mPrimedVars = new LinkedHashSet(iReqSymbolTable.getPrimedVars()); + mHistoryVars = new LinkedHashSet(iReqSymbolTable.getHistoryVars()); + mEventVars = new LinkedHashSet(iReqSymbolTable.getEventVars()); + mPcVars = new LinkedHashSet(iReqSymbolTable.getPcVars()); + mClockVars = new LinkedHashSet(iReqSymbolTable.getClockVars()); + + mReq2Loc = new LinkedHashMap<>(); + mConst2Value = new LinkedHashMap<>(iReqSymbolTable.getConstToValue()); + mInputVars = new LinkedHashSet<>(iReqSymbolTable.getInputVars()); + mOutputVars = new LinkedHashSet<>(iReqSymbolTable.getOutputVars()); + mEquivalences = iReqSymbolTable.getVariableEquivalenceClasses(); + mBuiltinFunctions = generateBuildinFuntions(); + } + public void addInitPattern(final DeclarationPattern initPattern) { final BoogiePrimitiveType type = BoogiePrimitiveType.toPrimitiveType(initPattern.getType()); @@ -198,13 +238,13 @@ private void updateEquivalences(final PhaseEventAutomata pea) { mEquivalences.union(peaVars); } - public void addAuxvar(final String name, final String typeString, final PatternType source) { + public void addAuxVarPrimedAndUnprimed(final String name, final String typeString, final PatternType source) { addVar(name, BoogiePrimitiveType.toPrimitiveType(typeString), source, mStateVars); } public IReqSymbolTable constructSymbolTable() { final String deltaVar = declareDeltaVar(); - return new ReqSymbolTable(deltaVar, mId2Type, mId2IdExpr, mId2VarLHS, mStateVars, mPrimedVars, mHistoryVars, + return new ReqSymbolTable(deltaVar, mId2Type, mId2IdExpr, mId2VarLHS, mAuxStatements, mAuxVars, mStateVars, mPrimedVars, mHistoryVars, mConstVars, mEventVars, mPcVars, mClockVars, mReq2Loc, mConst2Value, mInputVars, mOutputVars, mBuiltinFunctions, mEquivalences); } @@ -255,6 +295,24 @@ private void addVar(final String name, final BoogieType type, final PatternType< addVarOneKind(getHistoryVarId(name), type, source, mHistoryVars); addVarOneKind(getPrimedVarId(name), type, source, mPrimedVars); } + + public AuxStatement addAuxVar(final AuxStatement auxStatement, final String name, final String boogieType, final PatternType source) { + Set kind = mAuxVars; + auxStatement.setBoogieLocation(DUMMY_LOC); + switch (boogieType.toLowerCase()) { + case "bool": + case "real": + case "int": + addVarOneKind(name, BoogiePrimitiveType.toPrimitiveType(boogieType), source, kind); + return mAuxStatements.addAuxStatement(name, auxStatement); + case "event": + break; + default: + addError(name, new ErrorInfo(ErrorType.UNKNOWN_TYPE, source)); + break; + } + return null; + } private void addVarOneKind(final String name, final BoogieType type, final PatternType source, final Set kind) { @@ -348,6 +406,9 @@ private static final class ReqSymbolTable implements IReqSymbolTable { private final Map mId2VarLHS; private final Map mConst2Value; private final Map, BoogieLocation> mReq2Loc; + + private final AuxStatementContainer mAuxStatements; + private final Set mAuxVars; private final Set mStateVars; private final Set mConstVars; private final Set mPrimedVars; @@ -362,8 +423,8 @@ private static final class ReqSymbolTable implements IReqSymbolTable { private final UnionFind mEquivalences; private ReqSymbolTable(final String deltaVar, final Map id2Type, - final Map id2idExp, final Map id2VarLhs, - final Set stateVars, final Set primedVars, final Set historyVars, + final Map id2idExp, final Map id2VarLhs, final AuxStatementContainer auxStatements, + final Set auxVars, Set stateVars, final Set primedVars, final Set historyVars, final Set constVars, final Set eventVars, final Set pcVars, final Set clockVars, final Map, BoogieLocation> req2loc, final Map const2Value, final Set inputVars, final Set outputVars, @@ -372,6 +433,8 @@ private ReqSymbolTable(final String deltaVar, final Map id2T mId2IdExpr = Collections.unmodifiableMap(id2idExp); mId2VarLHS = Collections.unmodifiableMap(id2VarLhs); + mAuxStatements = auxStatements; + mAuxVars = Collections.unmodifiableSet(auxVars); mStateVars = Collections.unmodifiableSet(stateVars); mConstVars = Collections.unmodifiableSet(constVars); mPrimedVars = Collections.unmodifiableSet(primedVars); @@ -462,6 +525,21 @@ public Set getOutputVars() { public Map getConstToValue() { return mConst2Value; } + + @Override + public UnionFind getVariableEquivalenceClasses() { + return mEquivalences; + } + + @Override + public Set getAuxVars() { + return mAuxVars; + } + + @Override + public AuxStatementContainer getAuxStatementContainer( ) { + return mAuxStatements; + } @Override public String getPcName(final PhaseEventAutomata automaton) { @@ -489,6 +567,7 @@ public Collection getDeclarations() { decls.addAll(constructVariableDeclarations(mPrimedVars)); decls.addAll(constructVariableDeclarations(mHistoryVars)); decls.addAll(constructVariableDeclarations(mEventVars)); + decls.addAll(constructVariableDeclarations(mAuxVars)); decls.addAll(mBuildinFunctions.values()); return decls; } @@ -522,7 +601,7 @@ private List constructConstDeclarations(final Collection id final IdentifierExpression idExpr = mId2IdExpr.get(id); final Expression axiom = new BinaryExpression(value.getLoc(), value.getType(), Operator.COMPEQ, idExpr, value); - rtr.add(new Axiom(varlist.getLocation(), EMPTY_ATTRIBUTES, axiom)); + rtr.add(new Axiom(varlist.getLocation(), EMPTY_ATTRIBUTES, axiom)); } } return rtr; @@ -552,11 +631,6 @@ private List constructVarLists(final Collection ident return identifiers.stream().map(this::constructVarlist).filter(a -> a != null).collect(Collectors.toList()); } - @Override - public UnionFind getVariableEquivalenceClasses() { - return mEquivalences; - } - } public enum ErrorType { diff --git a/trunk/source/ReqToTest/src/de/uni_freiburg/informatik/ultimate/reqtotest/req/Req2TestReqSymbolTable.java b/trunk/source/ReqToTest/src/de/uni_freiburg/informatik/ultimate/reqtotest/req/Req2TestReqSymbolTable.java index 9cc5fa57671..6812a739f0e 100644 --- a/trunk/source/ReqToTest/src/de/uni_freiburg/informatik/ultimate/reqtotest/req/Req2TestReqSymbolTable.java +++ b/trunk/source/ReqToTest/src/de/uni_freiburg/informatik/ultimate/reqtotest/req/Req2TestReqSymbolTable.java @@ -37,6 +37,7 @@ import de.uni_freiburg.informatik.ultimate.logic.FunctionSymbol; import de.uni_freiburg.informatik.ultimate.logic.TermVariable; import de.uni_freiburg.informatik.ultimate.pea2boogie.IReqSymbolTable; +import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.AuxStatementContainer; import de.uni_freiburg.informatik.ultimate.reqtotest.graphtransformer.FakeBoogieVar; import de.uni_freiburg.informatik.ultimate.util.datastructures.UnionFind; @@ -128,10 +129,6 @@ public Set getConstVars() { return mConstVars; } - public Set getAuxVars() { - return mAuxVars; - } - @Override public Set getHistoryVars() { return mHistoryVars; @@ -367,4 +364,16 @@ public UnionFind getVariableEquivalenceClasses() { throw new UnsupportedOperationException(); } + @Override + public Set getAuxVars() { + // TODO Auto-generated method stub + return null; + } + + @Override + public AuxStatementContainer getAuxStatementContainer() { + // TODO Auto-generated method stub + return null; + } + } From 6c8af66d854df1acc7760baa8d65635858a63d84 Mon Sep 17 00:00:00 2001 From: Tob1as864 <76437441+Tob1as864@users.noreply.github.com> Date: Tue, 15 Aug 2023 20:21:37 +0200 Subject: [PATCH 02/23] Update trunk/source/Library-UltimateModel/src/de/uni_freiburg/informatik/ultimate/core/model/preferences/UltimatePreferenceItem.java Co-authored-by: Manuel Bentele --- .../core/model/preferences/UltimatePreferenceItem.java | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/trunk/source/Library-UltimateModel/src/de/uni_freiburg/informatik/ultimate/core/model/preferences/UltimatePreferenceItem.java b/trunk/source/Library-UltimateModel/src/de/uni_freiburg/informatik/ultimate/core/model/preferences/UltimatePreferenceItem.java index 6fa7e6e2d52..409a90d863e 100644 --- a/trunk/source/Library-UltimateModel/src/de/uni_freiburg/informatik/ultimate/core/model/preferences/UltimatePreferenceItem.java +++ b/trunk/source/Library-UltimateModel/src/de/uni_freiburg/informatik/ultimate/core/model/preferences/UltimatePreferenceItem.java @@ -217,7 +217,8 @@ public StringValidator(String pattern) { @Override public boolean isValid(final String string) { - String[]exprPairs = string.split(","); + String[]exprPairs = string.split(","); + for(String exprPair : exprPairs) { Matcher m = match(exprPair, mPattern); if(!m.matches()) { From 3de1715b24f36a817e62d4f66cb490d1471cae0e Mon Sep 17 00:00:00 2001 From: Tob1as864 <76437441+Tob1as864@users.noreply.github.com> Date: Tue, 15 Aug 2023 20:26:04 +0200 Subject: [PATCH 03/23] Update trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/generator/RtInconcistencyConditionGenerator.java Co-authored-by: Manuel Bentele --- .../generator/RtInconcistencyConditionGenerator.java | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/generator/RtInconcistencyConditionGenerator.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/generator/RtInconcistencyConditionGenerator.java index 09388596c13..d600d308dbc 100644 --- a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/generator/RtInconcistencyConditionGenerator.java +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/generator/RtInconcistencyConditionGenerator.java @@ -307,8 +307,7 @@ private static Script buildSolver(final IUltimateServiceProvider services) throw * */ public Expression generateNonDeadlockCondition(final PhaseEventAutomata[] automata) { - //if (PRINT_PEA_DOT) { - if (true) { + if (PRINT_PEA_DOT) { mLogger.info("### Printing DOT for Peas ###"); for (int i = 0; i < automata.length; ++i) { final PhaseEventAutomata pea = automata[i]; From b531f42bfaeab19e9be639c891e2b788283f674d Mon Sep 17 00:00:00 2001 From: Tob1as864 <76437441+Tob1as864@users.noreply.github.com> Date: Tue, 15 Aug 2023 20:28:07 +0200 Subject: [PATCH 04/23] Update trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/preferences/Pea2BoogiePreferences.java Co-authored-by: Manuel Bentele --- .../ultimate/pea2boogie/preferences/Pea2BoogiePreferences.java | 1 - 1 file changed, 1 deletion(-) diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/preferences/Pea2BoogiePreferences.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/preferences/Pea2BoogiePreferences.java index 703e8513440..a3241088585 100644 --- a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/preferences/Pea2BoogiePreferences.java +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/preferences/Pea2BoogiePreferences.java @@ -57,7 +57,6 @@ public class Pea2BoogiePreferences extends UltimatePreferenceInitializer { public static final String LABEL_CHECK_RT_INCONSISTENCY = "Check rt-inconsistency"; private static final boolean DEF_CHECK_RT_INCONSISTENCY = true; private static final String DESC_CHECK_RT_INCONSISTENCY = null; - public static final String LABEL_USE_EPSILON = "Use epsilon transformation during rt-inconsistency check"; private static final boolean DEF_USE_EPSILON = true; private static final String DESC_USE_EPSILON = null; From b4aa9f54b124b781b42f68f3885f0bcb8ae78867 Mon Sep 17 00:00:00 2001 From: Tob1as864 <76437441+Tob1as864@users.noreply.github.com> Date: Tue, 15 Aug 2023 20:29:32 +0200 Subject: [PATCH 05/23] Update trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/req2pea/ReqCheckAnnotator.java Co-authored-by: Manuel Bentele --- .../ultimate/pea2boogie/req2pea/ReqCheckAnnotator.java | 1 - 1 file changed, 1 deletion(-) diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/req2pea/ReqCheckAnnotator.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/req2pea/ReqCheckAnnotator.java index 23b95b24b5c..7709d2face5 100644 --- a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/req2pea/ReqCheckAnnotator.java +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/req2pea/ReqCheckAnnotator.java @@ -197,7 +197,6 @@ private List generateAnnotations() { private List genCheckStateRecoverability(final BoogieLocation bl) { List list = new ArrayList<>(); StateRecoverabilityGenerator mStRecGen = new StateRecoverabilityGenerator(); - //Set consideredPcLocations = mStRecGen.getRelevantLocationsFromPea(mReqPeas); AuxStatementContainer auxStatementContainer = mSymbolTable.getAuxStatementContainer(); Map>> vePeaAuxStatementMap = mStRecGen.getAuxStatementPerVerificationExpression(auxStatementContainer); From 3096f1e42a86f03be27f21fb1a08c3dc85bd584a Mon Sep 17 00:00:00 2001 From: Tob1as864 <76437441+Tob1as864@users.noreply.github.com> Date: Tue, 15 Aug 2023 20:31:30 +0200 Subject: [PATCH 06/23] Update trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/req2pea/ReqCheckAnnotator.java Co-authored-by: Manuel Bentele --- .../ultimate/pea2boogie/req2pea/ReqCheckAnnotator.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/req2pea/ReqCheckAnnotator.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/req2pea/ReqCheckAnnotator.java index 7709d2face5..38b642e8837 100644 --- a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/req2pea/ReqCheckAnnotator.java +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/req2pea/ReqCheckAnnotator.java @@ -318,7 +318,7 @@ private Statement genAssertRTInconsistency(final Entry, PhaseEven final PhaseEventAutomata[] automata = automataSet.toArray(new PhaseEventAutomata[subset.length]); final Expression expr = mRtInconcistencyConditionGenerator.generateNonDeadlockCondition(automata); - final ReqCheck check = createReqCheck(Spec.RTINCONSISTENT,"", subset); + final ReqCheck check = createReqCheck(Spec.RTINCONSISTENT, "", subset); if (expr == null) { if (mReportTrivialConsistency) { From 9d4e8be4150045c3f47c5f91e96a9b20ffce8da8 Mon Sep 17 00:00:00 2001 From: Tob1as864 <76437441+Tob1as864@users.noreply.github.com> Date: Tue, 15 Aug 2023 20:33:25 +0200 Subject: [PATCH 07/23] Update trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/AuxStatement.java Co-authored-by: Manuel Bentele --- .../pea2boogie/staterecoverability/AuxStatement.java | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/AuxStatement.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/AuxStatement.java index acb7d5158aa..f85d8973fcc 100644 --- a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/AuxStatement.java +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/AuxStatement.java @@ -9,7 +9,7 @@ public interface AuxStatement { -public Statement getStatement(StRecExpr stRecExpr); -public BoogieLocation setBoogieLocation(BoogieLocation loc); -public BoogieLocation getBoogieLocation(); + public Statement getStatement(StRecExpr stRecExpr); + public BoogieLocation setBoogieLocation(BoogieLocation loc); + public BoogieLocation getBoogieLocation(); } From 3ed0ed05b177eaf1dac4be5d2cbbfba623a4b6a7 Mon Sep 17 00:00:00 2001 From: Tob1as864 <76437441+Tob1as864@users.noreply.github.com> Date: Tue, 15 Aug 2023 20:36:01 +0200 Subject: [PATCH 08/23] Update trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/translator/Req2BoogieTranslator.java Co-authored-by: Manuel Bentele --- .../ultimate/pea2boogie/translator/Req2BoogieTranslator.java | 1 - 1 file changed, 1 deletion(-) diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/translator/Req2BoogieTranslator.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/translator/Req2BoogieTranslator.java index d5aa79102e1..9120307ba3b 100644 --- a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/translator/Req2BoogieTranslator.java +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/translator/Req2BoogieTranslator.java @@ -560,7 +560,6 @@ private Statement[] genWhileLoopBody(final BoogieLocation bl) { } } // Assign St-Recoverability if statement - //stmtList.addAll(mSymboltable.getAuxStatements().setBoogieLocationForInstance(new StateRecoverabilityAuxStatement(""), StRecExpr.IF_ST, bl)); stmtList.addAll(mSymboltable.getAuxStatementContainer().getStatements(StRecExpr.IF_ST)); stmtList.addAll(mReqCheckAnnotator.getStateChecks()); stmtList.addAll( From 39b357fba7fdb85428d7b53d5fd0adeef2dac945 Mon Sep 17 00:00:00 2001 From: Tob1as864 <76437441+Tob1as864@users.noreply.github.com> Date: Tue, 15 Aug 2023 20:36:44 +0200 Subject: [PATCH 09/23] Update trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/translator/Req2BoogieTranslator.java Co-authored-by: Manuel Bentele --- .../ultimate/pea2boogie/translator/Req2BoogieTranslator.java | 1 - 1 file changed, 1 deletion(-) diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/translator/Req2BoogieTranslator.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/translator/Req2BoogieTranslator.java index 9120307ba3b..57c252f7f7d 100644 --- a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/translator/Req2BoogieTranslator.java +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/translator/Req2BoogieTranslator.java @@ -564,7 +564,6 @@ private Statement[] genWhileLoopBody(final BoogieLocation bl) { stmtList.addAll(mReqCheckAnnotator.getStateChecks()); stmtList.addAll( mSymboltable.getPcVars().stream().map(this::genStateVarAssignHistory).collect(Collectors.toList())); - for (final ReqPeas reqpea : mReqPeas) { for (final Entry ct2pea : reqpea.getCounterTrace2Pea()) { final PhaseEventAutomata pea = ct2pea.getValue(); From 177838a8cb017e02e28bbacf8dd4f74ca0a3c8b8 Mon Sep 17 00:00:00 2001 From: Tobias Wiessner Date: Tue, 15 Aug 2023 21:29:30 +0200 Subject: [PATCH 10/23] Fixes for pull request --- .../pea2boogie/PEAtoBoogieObserver.java | 20 +- .../VerificationResultTransformer.java | 9 +- .../RtInconcistencyConditionGenerator.java | 3 +- .../preferences/Pea2BoogiePreferences.java | 1 - .../pea2boogie/req2pea/ReqCheckAnnotator.java | 6 +- .../ultimate/pea2boogie/results/ReqCheck.java | 2 +- .../staterecoverability/AuxStatement.java | 10 +- .../PeaPhaseProgramCounter.java | 2 +- .../StateRecoverabilityGenerator.java | 228 ++++++++++-------- .../VerificationExpressionContainer.java | 137 +++++------ .../translator/Req2BoogieTranslator.java | 2 - 11 files changed, 217 insertions(+), 203 deletions(-) diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/PEAtoBoogieObserver.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/PEAtoBoogieObserver.java index d36b66ec1c6..cbb46891a70 100644 --- a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/PEAtoBoogieObserver.java +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/PEAtoBoogieObserver.java @@ -56,7 +56,7 @@ private IElement generateBoogie(final List> patterns) { if (mode == PEATransformerMode.REQ_CHECK) { return generateReqCheckBoogie(patterns); } - if(mode == PEATransformerMode.REQ_PARAM_CHECK) { + if (mode == PEATransformerMode.REQ_PARAM_CHECK) { return generateReqParamCheckBoogie(patterns); } if (mode == PEATransformerMode.REQ_TEST) { @@ -66,7 +66,8 @@ private IElement generateBoogie(final List> patterns) { } private IElement generateReqCheckBoogie(final List> patterns) { - final Req2BoogieTranslator translator = new Req2BoogieTranslator(mServices, mLogger, patterns, Collections.emptyList()); + final Req2BoogieTranslator translator = + new Req2BoogieTranslator(mServices, mLogger, patterns, Collections.emptyList()); final VerificationResultTransformer reporter = new VerificationResultTransformer(mLogger, mServices, translator.getReqSymbolTable()); // register CEX transformer that removes program executions from CEX. @@ -74,13 +75,16 @@ private IElement generateReqCheckBoogie(final List> patterns) { mServices.getResultService().registerTransformer("CexReducer", resultTransformer); return translator.getUnit(); } - + private IElement generateReqParamCheckBoogie(final List> patterns) { - final Req2ModifySymbolTablePeaTransformer transformer = new Req2ModifySymbolTablePeaTransformer(mServices, mLogger); - - final Req2BoogieTranslator translator = new Req2BoogieTranslator(mServices, mLogger, patterns, Collections.singletonList(transformer)); - - final VerificationResultTransformer reporter = new VerificationResultTransformer(mLogger, mServices, translator.getReqSymbolTable()); + final Req2ModifySymbolTablePeaTransformer transformer = + new Req2ModifySymbolTablePeaTransformer(mServices, mLogger); + + final Req2BoogieTranslator translator = + new Req2BoogieTranslator(mServices, mLogger, patterns, Collections.singletonList(transformer)); + + final VerificationResultTransformer reporter = + new VerificationResultTransformer(mLogger, mServices, translator.getReqSymbolTable()); // register CEX transformer that removes program executions from CEX. final UnaryOperator resultTransformer = reporter::convertTraceAbstractionResult; mServices.getResultService().registerTransformer("CexReducer", resultTransformer); diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/VerificationResultTransformer.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/VerificationResultTransformer.java index 1f9903baadc..a36be049172 100644 --- a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/VerificationResultTransformer.java +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/VerificationResultTransformer.java @@ -190,12 +190,13 @@ public IResult convertTraceAbstractionResult(final IResult result) { final String failurePath = formatTimeSequenceMap(delta2var2value); return new ReqCheckRtInconsistentResult<>(element, plugin, translatorSequence, failurePath); } - - if(spec == Spec.STATE_RECOVERABILITY) { + + if (spec == Spec.STATE_RECOVERABILITY) { IBacktranslationService translatorSequenceStRec = oldRes.getCurrentBacktranslation(); - return new ReqCheckStateRecoverabilityResult<>(element, plugin, translatorSequenceStRec, reqCheck.getMessage()); + return new ReqCheckStateRecoverabilityResult<>(element, plugin, translatorSequenceStRec, + reqCheck.getMessage()); } - + return new ReqCheckFailResult<>(element, plugin, translatorSequence); } diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/generator/RtInconcistencyConditionGenerator.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/generator/RtInconcistencyConditionGenerator.java index 09388596c13..d600d308dbc 100644 --- a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/generator/RtInconcistencyConditionGenerator.java +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/generator/RtInconcistencyConditionGenerator.java @@ -307,8 +307,7 @@ private static Script buildSolver(final IUltimateServiceProvider services) throw * */ public Expression generateNonDeadlockCondition(final PhaseEventAutomata[] automata) { - //if (PRINT_PEA_DOT) { - if (true) { + if (PRINT_PEA_DOT) { mLogger.info("### Printing DOT for Peas ###"); for (int i = 0; i < automata.length; ++i) { final PhaseEventAutomata pea = automata[i]; diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/preferences/Pea2BoogiePreferences.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/preferences/Pea2BoogiePreferences.java index 703e8513440..a3241088585 100644 --- a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/preferences/Pea2BoogiePreferences.java +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/preferences/Pea2BoogiePreferences.java @@ -57,7 +57,6 @@ public class Pea2BoogiePreferences extends UltimatePreferenceInitializer { public static final String LABEL_CHECK_RT_INCONSISTENCY = "Check rt-inconsistency"; private static final boolean DEF_CHECK_RT_INCONSISTENCY = true; private static final String DESC_CHECK_RT_INCONSISTENCY = null; - public static final String LABEL_USE_EPSILON = "Use epsilon transformation during rt-inconsistency check"; private static final boolean DEF_USE_EPSILON = true; private static final String DESC_USE_EPSILON = null; diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/req2pea/ReqCheckAnnotator.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/req2pea/ReqCheckAnnotator.java index 23b95b24b5c..ee90c63b303 100644 --- a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/req2pea/ReqCheckAnnotator.java +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/req2pea/ReqCheckAnnotator.java @@ -186,7 +186,6 @@ private List generateAnnotations() { annotations.addAll(genChecksNonVacuity(mUnitLocation)); } annotations.addAll(genChecksRTInconsistency(mUnitLocation)); - //New check if(mCheckStateRecoverability) { annotations.addAll(genCheckStateRecoverability(mUnitLocation)); } @@ -197,7 +196,6 @@ private List generateAnnotations() { private List genCheckStateRecoverability(final BoogieLocation bl) { List list = new ArrayList<>(); StateRecoverabilityGenerator mStRecGen = new StateRecoverabilityGenerator(); - //Set consideredPcLocations = mStRecGen.getRelevantLocationsFromPea(mReqPeas); AuxStatementContainer auxStatementContainer = mSymbolTable.getAuxStatementContainer(); Map>> vePeaAuxStatementMap = mStRecGen.getAuxStatementPerVerificationExpression(auxStatementContainer); @@ -223,10 +221,8 @@ private List genCheckStateRecoverability(final BoogieLocation bl) { // DOT printen final List, PhaseEventAutomata>> counterTracePEAList = new ArrayList<>(); for (final ReqPeas reqPea : mReqPeas) { - //Pattern mit Anforderung als Key final PatternType pattern = reqPea.getPattern(); - //Nötig weil komplexere Anforderungen mehrere DC haben können for (final Entry pea : reqPea.getCounterTrace2Pea()) { counterTracePEAList.add(new Pair<>(pattern, pea.getValue())); } @@ -319,7 +315,7 @@ private Statement genAssertRTInconsistency(final Entry, PhaseEven final PhaseEventAutomata[] automata = automataSet.toArray(new PhaseEventAutomata[subset.length]); final Expression expr = mRtInconcistencyConditionGenerator.generateNonDeadlockCondition(automata); - final ReqCheck check = createReqCheck(Spec.RTINCONSISTENT,"", subset); + final ReqCheck check = createReqCheck(Spec.RTINCONSISTENT, "", subset); if (expr == null) { if (mReportTrivialConsistency) { diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/results/ReqCheck.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/results/ReqCheck.java index ebbec7a25e5..73ce3a3a52f 100644 --- a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/results/ReqCheck.java +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/results/ReqCheck.java @@ -140,7 +140,7 @@ public ReqCheck merge(final ReqCheck other) { } private String createMessage() { - if(mMessage.isEmpty()) { + if(mMessage == null) { return ""; } return mMessage; diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/AuxStatement.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/AuxStatement.java index acb7d5158aa..d12e40bde2c 100644 --- a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/AuxStatement.java +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/AuxStatement.java @@ -8,8 +8,10 @@ import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.AuxStatementContainer.StRecExpr; public interface AuxStatement { - -public Statement getStatement(StRecExpr stRecExpr); -public BoogieLocation setBoogieLocation(BoogieLocation loc); -public BoogieLocation getBoogieLocation(); + + public Statement getStatement(StRecExpr stRecExpr); + + public BoogieLocation setBoogieLocation(BoogieLocation loc); + + public BoogieLocation getBoogieLocation(); } diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/PeaPhaseProgramCounter.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/PeaPhaseProgramCounter.java index 364e035708d..c1d2d481a49 100644 --- a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/PeaPhaseProgramCounter.java +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/PeaPhaseProgramCounter.java @@ -16,7 +16,7 @@ public class PeaPhaseProgramCounter { private final PhaseEventAutomata pea; private final PatternType req; - public PeaPhaseProgramCounter(int pc, Phase phase, PhaseEventAutomata pea, PatternType req) { + public PeaPhaseProgramCounter(final int pc, final Phase phase, final PhaseEventAutomata pea, final PatternType req) { super(); this.pc = pc; this.phase = phase; diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/StateRecoverabilityGenerator.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/StateRecoverabilityGenerator.java index 7d66c870c3c..795bee8b9f4 100644 --- a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/StateRecoverabilityGenerator.java +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/StateRecoverabilityGenerator.java @@ -63,7 +63,7 @@ import de.uni_freiburg.informatik.ultimate.util.ConstructionCache; public class StateRecoverabilityGenerator { - + private IReqSymbolTable mReqSymboltable; private Term mPrimedInvariant; private Script mScript; @@ -77,74 +77,79 @@ public class StateRecoverabilityGenerator { private BoogieDeclarations boogieDeclarations; private ConstructionCache mPossibleStartLocations; - - public StateRecoverabilityGenerator( ) { + + public StateRecoverabilityGenerator() { } - - public StateRecoverabilityGenerator(final ILogger logger, final IUltimateServiceProvider services, final IReqSymbolTable symboltable) { + + public StateRecoverabilityGenerator(final ILogger logger, final IUltimateServiceProvider services, + final IReqSymbolTable symboltable) { mReqSymboltable = symboltable; mServices = services; mLogger = logger; - + mPeaResultUtil = new PeaResultUtil(mLogger, mServices); mScript = buildSolver(services); mManagedScript = new ManagedScript(services, mScript); - + boogieDeclarations = new BoogieDeclarations(mReqSymboltable.getDeclarations(), mLogger); mBoogie2Smt = new Boogie2SMT(mManagedScript, boogieDeclarations, services, false); mVars = mBoogie2Smt.getBoogie2SmtSymbolTable().getGlobalsMap(); - + mPossibleStartLocations = new ConstructionCache<>(this::constructSearchStartLocationTerm); mCddToSmt = new CddToSmt(mServices, mPeaResultUtil, mScript, mBoogie2Smt, boogieDeclarations, mReqSymboltable); } - - public Map> getRelevantLocationsFromPea(List reqPeasList, VerificationExpressionContainer vec) { + + public Map> + getRelevantLocationsFromPea(List reqPeasList, VerificationExpressionContainer vec) { Map> veLocation = new HashMap<>(); Set reqPeasSet = new HashSet<>(reqPeasList); Set declaredConstants = new HashSet<>(); - Map reqPeasTerm = new HashMap<>(); - + Map reqPeasTerm = new HashMap<>(); + // Create Terms for every location - for(ReqPeas reqPeas : reqPeasList) { + for (ReqPeas reqPeas : reqPeasList) { List> ctPeaList = reqPeas.getCounterTrace2Pea(); Term parallelAutomaton = generateParallelAutomatonTerm(removeReqPeas(reqPeasSet, reqPeas)); reqPeasTerm.put(reqPeas, parallelAutomaton); } - - for(ReqPeas reqPea : reqPeasList) { + + for (ReqPeas reqPea : reqPeasList) { List> ctPeaList = reqPea.getCounterTrace2Pea(); PatternType req = reqPea.getPattern(); - for(Entry entry : ctPeaList) { + for (Entry entry : ctPeaList) { Phase[] phases = entry.getValue().getPhases(); - for(int i = 0; i < phases.length; ++i) { - Phase phase = phases[i]; + for (int i = 0; i < phases.length; ++i) { + Phase phase = phases[i]; // Check for every phase if the location can fulfill the verification expression // TRUE -> Do not add the phase // FALSE -> Add the phase - for(VerificationExpression ve : vec.getVerificationExpressions().values()) { - CDD veCcd = BoogieBooleanExpressionDecision.create(createOppositeCondition(new DefaultLocation(), ve.getBoogiePrimitiveType(), ve.getVariable(), ve.getOperator(), ve.getValue())); + for (VerificationExpression ve : vec.getVerificationExpressions().values()) { + CDD veCcd = BoogieBooleanExpressionDecision + .create(createOppositeCondition(new DefaultLocation(), ve.getBoogiePrimitiveType(), + ve.getVariable(), ve.getOperator(), ve.getValue())); List invariantVeList = new ArrayList<>(); - + // Compute phase invariant ⋀ opposite verification expression final Term termVe = mCddToSmt.toSmt(veCcd); invariantVeList.add(termVe); final Term termLocation = mCddToSmt.toSmt(phase.getStateInvariant()); invariantVeList.add(termLocation); - - //Find satisfiable model + + // Find satisfiable model final Term termModel = SmtUtils.and(mScript, invariantVeList); - if(SmtUtils.checkSatTerm(mScript, termModel) == LBool.SAT) { - if(!veLocation.containsKey(ve)) { + if (SmtUtils.checkSatTerm(mScript, termModel) == LBool.SAT) { + if (!veLocation.containsKey(ve)) { veLocation.put(ve, new HashSet<>()); } - - Term possibleStartPhase = possibleStartPhase(phase, reqPea, reqPeasTerm.get(reqPea), termVe); - + + Term possibleStartPhase = + possibleStartPhase(phase, reqPea, reqPeasTerm.get(reqPea), termVe); + // Declare constants for Z3 declareConstants(mScript, possibleStartPhase, declaredConstants); - - if(SmtUtils.checkSatTerm(mScript, possibleStartPhase) == LBool.SAT) { + + if (SmtUtils.checkSatTerm(mScript, possibleStartPhase) == LBool.SAT) { veLocation.get(ve).add(new PeaPhaseProgramCounter(i, phase, entry.getValue(), req)); } } @@ -154,88 +159,89 @@ public Map> getRelevantLocat } return veLocation; } - + private void declareConstants(Script script, Term term, Set declaredConstants) { Sort sort = term.getSort(); TermVariable[] termVariables = term.getFreeVars(); - for(int i = 0; i < termVariables.length; ++i) { - //mScript.declareFun("ENG_READY", new Sort[0], sort); + for (int i = 0; i < termVariables.length; ++i) { + // mScript.declareFun("ENG_READY", new Sort[0], sort); TermVariable termVariable = termVariables[i]; - if(!declaredConstants.contains(termVariable.getName())) { + if (!declaredConstants.contains(termVariable.getName())) { script.declareFun(termVariable.getName(), new Sort[0], sort); declaredConstants.add(termVariable.getName()); } } } - + private Term possibleStartPhase(Phase phase, ReqPeas reqPeas, Term parallelAutomaton, Term termVe) { Term actualTerm = generatePhaseTerm(phase); - Term[] terms = new Term[] {actualTerm, parallelAutomaton, termVe}; - + Term[] terms = new Term[] { actualTerm, parallelAutomaton, termVe }; + final Term finalTerm = termAnd(terms); return finalTerm; } - + private Term termAnd(Term[] terms) { final Term term = SmtUtils.and(mScript, terms); return term; } - + private Term generatePhaseTerm(Phase phase) { final Term term = mCddToSmt.toSmt(phase.getStateInvariant()); return term; } - + private Set removeReqPeas(Set reqPeasSet, ReqPeas reqPeas) { Set newReqPeasSet = new HashSet<>(reqPeasSet); newReqPeasSet.remove(reqPeas); return newReqPeasSet; } - + /** * Computes VE && (A_1 && A_2 && A_n && ...) * * A = ((p_1 && (g_1 || g_n)) || (p_2 && (g_n)) || ...) + * * @param reqPeas * @return term */ private Term generateParallelAutomatonTerm(Set reqPeas) { Map reqPeasPeaArrayMap = createPeaArray(reqPeas); CDD reqsCDD = null; - for(Map.Entry entry : reqPeasPeaArrayMap.entrySet()) { - + for (Map.Entry entry : reqPeasPeaArrayMap.entrySet()) { + // Automatons per requirement CDD peasCDD = null; PhaseEventAutomata[] peaArray = entry.getValue(); - for(PhaseEventAutomata pea : peaArray) { + for (PhaseEventAutomata pea : peaArray) { Phase[] phases = pea.getPhases(); - + // Create CDD for every location and guard CDD[] invariantPhaseGuardArrayPerPea = new CDD[pea.getPhases().length]; - for(int i = 0; i < invariantPhaseGuardArrayPerPea.length; ++i) { + for (int i = 0; i < invariantPhaseGuardArrayPerPea.length; ++i) { Phase phase = phases[i]; CDD invariantPhaseGuardCDD = phase.getStateInvariant().and(phase.getClockInvariant()); invariantPhaseGuardArrayPerPea[i] = invariantPhaseGuardCDD; } - + // Link every location-guard CDD with OR CDD peaCDD = null; - for(int i = 0; i < invariantPhaseGuardArrayPerPea.length; ++i) { - if(peaCDD == null) { + for (int i = 0; i < invariantPhaseGuardArrayPerPea.length; ++i) { + if (peaCDD == null) { peaCDD = invariantPhaseGuardArrayPerPea[i]; } peaCDD.or(invariantPhaseGuardArrayPerPea[i]); } - + // Link every pea with AND - if(peasCDD == null) { + if (peasCDD == null) { peasCDD = peaCDD; } else { peasCDD.and(peaCDD); } } // Link every req with AND - if(reqsCDD == null) { + if (reqsCDD == null) { reqsCDD = peasCDD; } else { reqsCDD.and(peasCDD); @@ -244,21 +250,23 @@ private Term generateParallelAutomatonTerm(Set reqPeas) { final Term term = mCddToSmt.toSmt(reqsCDD); return term; } + private Map createPeaArray(Set reqPeas) { Map reqPeasPeaArrayMap = new HashMap<>(); - for(ReqPeas reqPea : reqPeas) { + for (ReqPeas reqPea : reqPeas) { List> ctPeaList = reqPea.getCounterTrace2Pea(); - Set automataSet = ctPeaList.stream().map(Entry::getValue).collect(Collectors.toSet()); + Set automataSet = ctPeaList.stream() + .map(Entry::getValue).collect(Collectors.toSet()); final PhaseEventAutomata[] automata = automataSet.toArray(new PhaseEventAutomata[automataSet.size()]); reqPeasPeaArrayMap.put(reqPea, automata); } return reqPeasPeaArrayMap; } - + private Term constructSearchStartLocationTerm(Phase phase) { return transformAndLog(phase.getStateInvariant(), "phase invariant"); } - + private Term transformAndLog(final CDD org, final String msg) { final Term term = mCddToSmt.toSmt(org); mLogger.info("Can be start location %s %s", msg, org.toGeneralString()); @@ -267,58 +275,64 @@ private Term transformAndLog(final CDD org, final String msg) { private static Script buildSolver(final IUltimateServiceProvider services) throws AssertionError { SolverSettings settings = SolverBuilder.constructSolverSettings() - //.setSolverMode(SolverMode.External_ModelsAndUnsatCoreMode).setUseExternalSolver(ExternalSolver.Z3); + // .setSolverMode(SolverMode.External_ModelsAndUnsatCoreMode).setUseExternalSolver(ExternalSolver.Z3); .setSolverMode(SolverMode.External_ModelsMode).setUseExternalSolver(ExternalSolver.Z3); return SolverBuilder.buildAndInitializeSolver(services, settings, "RtInconsistencySolver"); } - - public Map>> getAuxStatementPerVerificationExpression(AuxStatementContainer auxStatementContainer) { - Map>> vePeaAuxStatementMap = new HashMap<>(); - for(AuxStatement auxStatement : auxStatementContainer.getSreMap().values()) { - if(auxStatement instanceof StateRecoverabilityAuxStatement) { + + public Map>> + getAuxStatementPerVerificationExpression(AuxStatementContainer auxStatementContainer) { + Map>> vePeaAuxStatementMap = + new HashMap<>(); + for (AuxStatement auxStatement : auxStatementContainer.getSreMap().values()) { + if (auxStatement instanceof StateRecoverabilityAuxStatement) { StateRecoverabilityAuxStatement stRecAuxSt = (StateRecoverabilityAuxStatement) auxStatement; - if(!vePeaAuxStatementMap.containsKey(stRecAuxSt.getVerificationExpression())) { + if (!vePeaAuxStatementMap.containsKey(stRecAuxSt.getVerificationExpression())) { vePeaAuxStatementMap.put(stRecAuxSt.getVerificationExpression(), new HashMap<>()); } - Map> peaAuxStatementMap = vePeaAuxStatementMap.get(stRecAuxSt.getVerificationExpression()); - if(!peaAuxStatementMap.containsKey(stRecAuxSt.getPeaPhasePc().getPea())) { + Map> peaAuxStatementMap = + vePeaAuxStatementMap.get(stRecAuxSt.getVerificationExpression()); + if (!peaAuxStatementMap.containsKey(stRecAuxSt.getPeaPhasePc().getPea())) { peaAuxStatementMap.put(stRecAuxSt.getPeaPhasePc().getPea(), new HashSet<>()); } - Set stRecAuxStSet = peaAuxStatementMap.get(stRecAuxSt.getPeaPhasePc().getPea()); + Set stRecAuxStSet = + peaAuxStatementMap.get(stRecAuxSt.getPeaPhasePc().getPea()); stRecAuxStSet.add(stRecAuxSt); } } return vePeaAuxStatementMap; } - - public Expression createOppositeCondition(final ILocation loc, BoogieType boogieType, String lhs, String opr, String rhs) { + + public Expression createOppositeCondition(final ILocation loc, BoogieType boogieType, String lhs, String opr, + String rhs) { String newOpr = ""; switch (opr) { - case "==": - newOpr = "!="; - break; - case "!=": - newOpr = "=="; - break; - case "<": - newOpr = ">="; - break; - case ">": - newOpr = "<="; - break; - case "<=": - newOpr = ">"; - break; - case ">=": - newOpr = "<"; - break; - default: - throw new RuntimeException(getClass().getName() + "Could not parse token: " + opr); + case "==": + newOpr = "!="; + break; + case "!=": + newOpr = "=="; + break; + case "<": + newOpr = ">="; + break; + case ">": + newOpr = "<="; + break; + case "<=": + newOpr = ">"; + break; + case ">=": + newOpr = "<"; + break; + default: + throw new RuntimeException(getClass().getName() + "Could not parse token: " + opr); } return createExpression(loc, boogieType, lhs, newOpr, rhs); } - - public Expression createExpression(final ILocation loc, BoogieType boogieType, String sLhs, Operator opr, String sRhs) { + + public Expression createExpression(final ILocation loc, BoogieType boogieType, String sLhs, Operator opr, + String sRhs) { Expression rhs = null; Expression lhs; lhs = new IdentifierExpression(loc, boogieType, sLhs, DeclarationInformation.DECLARATIONINFO_GLOBAL); @@ -335,12 +349,13 @@ public Expression createExpression(final ILocation loc, BoogieType boogieType, S break; case "type-error": throw new RuntimeErrorException(null, getClass().getName() + ": " + boogieType + " no known data type."); - } + } Expression expression = ExpressionFactory.newBinaryExpression(loc, opr, lhs, rhs); return expression; } - - public Expression createExpression(final ILocation loc, BoogieType boogieType, String sLhs, String sOpr, String sRhs) { + + public Expression createExpression(final ILocation loc, BoogieType boogieType, String sLhs, String sOpr, + String sRhs) { Expression rhs = null; Expression lhs; BinaryExpression.Operator opr; @@ -358,12 +373,12 @@ public Expression createExpression(final ILocation loc, BoogieType boogieType, S break; case "type-error": throw new RuntimeErrorException(null, getClass().getName() + ": " + boogieType + " no known data type."); - } + } opr = getOperator(sOpr); Expression expression = ExpressionFactory.newBinaryExpression(loc, opr, lhs, rhs); return expression; } - + private BinaryExpression.Operator getOperator(String sOpr) { switch (sOpr) { case "||": @@ -373,20 +388,19 @@ private BinaryExpression.Operator getOperator(String sOpr) { case "&": return Operator.LOGICAND; case "==": - return Operator.COMPEQ; - case "!=": - return Operator.COMPNEQ; - case "<": - return Operator.COMPLT; - case ">": - return Operator.COMPGT; - case "<=": - return Operator.COMPLEQ; - case ">=": - return Operator.COMPGEQ; + return Operator.COMPEQ; + case "!=": + return Operator.COMPNEQ; + case "<": + return Operator.COMPLT; + case ">": + return Operator.COMPGT; + case "<=": + return Operator.COMPLEQ; + case ">=": + return Operator.COMPGEQ; default: throw new RuntimeErrorException(null, getClass().getName() + ": Could not parse operator."); } } } - diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/VerificationExpressionContainer.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/VerificationExpressionContainer.java index cc56e47c060..88e6b56d9d7 100644 --- a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/VerificationExpressionContainer.java +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/VerificationExpressionContainer.java @@ -16,82 +16,83 @@ import de.uni_freiburg.informatik.ultimate.pea2boogie.req2pea.IReq2Pea; public class VerificationExpressionContainer { - - //Pattern for input expression + + // Pattern for input expression public static final String exprPattern = "\\s{0,1}((\\w+)\\s*([<>=!][=]*)\\s*(\\w+))\\s{0,1}"; - - //Data types - public static final String BOOL = "bool"; - public static final String INT = "int"; - public static final String REAL = "real"; - + + // Data types + public static final String BOOL = "bool"; + public static final String INT = "int"; + public static final String REAL = "real"; + private IReq2Pea mReq2pea; private Map mVerificationExpressions; private Map mVariableDataTypeMap; - public VerificationExpressionContainer(IReq2Pea req2pea) { - mReq2pea = req2pea; - mVerificationExpressions = new HashMap<>(); - getDataTypeFromReq2Pea(req2pea); - } - - private void getDataTypeFromReq2Pea(IReq2Pea req2Pea) { - Map variableDataTypeMap = new HashMap<>(); - for(ReqPeas reqPeas : req2Pea.getReqPeas()) { - List> mReq = reqPeas.getCounterTrace2Pea(); - for(Entry entry : mReq) { - PhaseEventAutomata pea = entry.getValue(); - for(Map.Entry entryVariableDataType : pea.getVariables().entrySet()) { - //TODO anpassen abhängig davon was es noch für Datentypen gibt - variableDataTypeMap.put(entryVariableDataType.getKey(), entryVariableDataType.getValue()); - } - } - } - mVariableDataTypeMap = variableDataTypeMap; - } + public VerificationExpressionContainer(IReq2Pea req2pea) { + mReq2pea = req2pea; + mVerificationExpressions = new HashMap<>(); + getDataTypeFromReq2Pea(req2pea); + } + + private void getDataTypeFromReq2Pea(IReq2Pea req2Pea) { + Map variableDataTypeMap = new HashMap<>(); + for (ReqPeas reqPeas : req2Pea.getReqPeas()) { + List> mReq = reqPeas.getCounterTrace2Pea(); + for (Entry entry : mReq) { + PhaseEventAutomata pea = entry.getValue(); + for (Map.Entry entryVariableDataType : pea.getVariables().entrySet()) { + // TODO anpassen abhängig davon was es noch für Datentypen gibt + variableDataTypeMap.put(entryVariableDataType.getKey(), entryVariableDataType.getValue()); + } + } + } + mVariableDataTypeMap = variableDataTypeMap; + } + + public Map getVerificationExpressions() { + return mVerificationExpressions; + } + + public void addExpression(String inputExpr) { + List veList = new ArrayList<>(); + int grpVariable = 2; + int grpOperator = 3; + int grpValue = 4; + String[] exprArray = inputExpr.split(","); + for (String expr : exprArray) { + Matcher m = match(expr, exprPattern); + if (m.find()) { + String sVariable = m.group(grpVariable); + String sOperator = m.group(grpOperator); + String sValue = m.group(grpValue); + String dataType = mVariableDataTypeMap.get(sVariable); + if (dataType == null) { + throw new IllegalArgumentException( + getClass().getName() + " could not find data type for " + sVariable); + } + veList.add(new VerificationExpression(new String[] { sVariable, sOperator, sValue }, dataType)); + } + } + addVerificationExpression(veList); + } - public Map getVerificationExpressions() { - return mVerificationExpressions; - } - - public void addExpression(String inputExpr) { - List veList = new ArrayList<>(); - int grpVariable = 2; - int grpOperator = 3; - int grpValue = 4; - String[] exprArray = inputExpr.split(","); - for(String expr : exprArray) { - Matcher m = match(expr, exprPattern); - if(m.find()) { - String sVariable = m.group(grpVariable); - String sOperator = m.group(grpOperator); - String sValue = m.group(grpValue); - String dataType = mVariableDataTypeMap.get(sVariable); - if(dataType == null) { - throw new IllegalArgumentException(getClass().getName() + " could not find data type for " + sVariable); - } - veList.add(new VerificationExpression(new String[] {sVariable, sOperator, sValue}, dataType)); - } - } - addVerificationExpression(veList); - } + private void addVerificationExpression(List veList) { + for (VerificationExpression ve : veList) { + addVerificationExpression(ve); + } + } - private void addVerificationExpression(List veList) { - for(VerificationExpression ve : veList) { - addVerificationExpression(ve); - } - } + private void addVerificationExpression(VerificationExpression ve) { + if (mVerificationExpressions == null) { + mVerificationExpressions = new HashMap<>(); + } + mVerificationExpressions.put(ve.getVariable(), ve); + } - private void addVerificationExpression(VerificationExpression ve) { - if(mVerificationExpressions == null) { - mVerificationExpressions = new HashMap<>(); - } - mVerificationExpressions.put(ve.getVariable(), ve); - } - - private Matcher match(String s, String pattern) { + private Matcher match(String s, String pattern) { Pattern p = Pattern.compile(pattern); - Matcher m = p.matcher(s); - return m; + Matcher m = p.matcher(s); + return m; } } diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/translator/Req2BoogieTranslator.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/translator/Req2BoogieTranslator.java index d5aa79102e1..57c252f7f7d 100644 --- a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/translator/Req2BoogieTranslator.java +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/translator/Req2BoogieTranslator.java @@ -560,12 +560,10 @@ private Statement[] genWhileLoopBody(final BoogieLocation bl) { } } // Assign St-Recoverability if statement - //stmtList.addAll(mSymboltable.getAuxStatements().setBoogieLocationForInstance(new StateRecoverabilityAuxStatement(""), StRecExpr.IF_ST, bl)); stmtList.addAll(mSymboltable.getAuxStatementContainer().getStatements(StRecExpr.IF_ST)); stmtList.addAll(mReqCheckAnnotator.getStateChecks()); stmtList.addAll( mSymboltable.getPcVars().stream().map(this::genStateVarAssignHistory).collect(Collectors.toList())); - for (final ReqPeas reqpea : mReqPeas) { for (final Entry ct2pea : reqpea.getCounterTrace2Pea()) { final PhaseEventAutomata pea = ct2pea.getValue(); From a4857995b61e4589eccde012bf19d945f6a551c8 Mon Sep 17 00:00:00 2001 From: Tobias Wiessner Date: Tue, 15 Aug 2023 22:43:19 +0200 Subject: [PATCH 11/23] Fixes for review --- .../ultimate/pea2boogie/req2pea/ReqCheckAnnotator.java | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/req2pea/ReqCheckAnnotator.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/req2pea/ReqCheckAnnotator.java index ee90c63b303..821712e2a64 100644 --- a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/req2pea/ReqCheckAnnotator.java +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/req2pea/ReqCheckAnnotator.java @@ -219,6 +219,7 @@ private List genCheckStateRecoverability(final BoogieLocation bl) { } // DOT printen + /* final List, PhaseEventAutomata>> counterTracePEAList = new ArrayList<>(); for (final ReqPeas reqPea : mReqPeas) { final PatternType pattern = reqPea.getPattern(); @@ -229,8 +230,8 @@ private List genCheckStateRecoverability(final BoogieLocation bl) { } final List, PhaseEventAutomata>[]> subsets = CrossProducts.subArrays(counterTracePEAList.toArray(new Entry[counterTracePEAList.size()]), counterTracePEAList.size(), new Entry[counterTracePEAList.size()]); //Prints parallel automaton - //dotPrinter(subsets); - + dotPrinter(subsets); + */ return list; } From 3eac26a8392d0c0a2a408fc3534bf3abbaf786e7 Mon Sep 17 00:00:00 2001 From: Tobias Wiessner Date: Mon, 28 Aug 2023 17:21:06 +0200 Subject: [PATCH 12/23] Review fix --- .../preferences/UltimatePreferenceItem.java | 14 ++-- .../ultimate/pea2boogie/IReqSymbolTable.java | 10 +-- .../preferences/Pea2BoogiePreferences.java | 66 ++++++++++--------- .../pea2boogie/req2pea/ReqCheckAnnotator.java | 58 ++++++++-------- .../ultimate/pea2boogie/results/ReqCheck.java | 15 ++--- .../ReqCheckStateRecoverabilityResult.java | 2 +- ...Statement.java => AuxiliaryStatement.java} | 6 +- ....java => AuxiliaryStatementContainer.java} | 42 ++++++------ ...tateRecoverabilityAuxiliaryStatement.java} | 10 +-- .../StateRecoverabilityGenerator.java | 16 ++--- .../testgen/Req2ModifySymbolTablePea.java | 28 ++++---- .../translator/Req2BoogieTranslator.java | 10 +-- .../translator/ReqSymboltableBuilder.java | 16 ++--- .../reqtotest/req/Req2TestReqSymbolTable.java | 4 +- 14 files changed, 151 insertions(+), 146 deletions(-) rename trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/{AuxStatement.java => AuxiliaryStatement.java} (73%) rename trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/{AuxStatementContainer.java => AuxiliaryStatementContainer.java} (57%) rename trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/{StateRecoverabilityAuxStatement.java => StateRecoverabilityAuxiliaryStatement.java} (85%) diff --git a/trunk/source/Library-UltimateModel/src/de/uni_freiburg/informatik/ultimate/core/model/preferences/UltimatePreferenceItem.java b/trunk/source/Library-UltimateModel/src/de/uni_freiburg/informatik/ultimate/core/model/preferences/UltimatePreferenceItem.java index 6fa7e6e2d52..118bda4d75b 100644 --- a/trunk/source/Library-UltimateModel/src/de/uni_freiburg/informatik/ultimate/core/model/preferences/UltimatePreferenceItem.java +++ b/trunk/source/Library-UltimateModel/src/de/uni_freiburg/informatik/ultimate/core/model/preferences/UltimatePreferenceItem.java @@ -206,7 +206,7 @@ public String getInvalidValueErrorMessage(final Double value) { return "Valid range is " + mMin + " <= value <= " + mMax; } } - + public class StringValidator implements IUltimatePreferenceItemValidator { private final String mPattern; @@ -217,10 +217,10 @@ public StringValidator(String pattern) { @Override public boolean isValid(final String string) { - String[]exprPairs = string.split(","); - for(String exprPair : exprPairs) { + String[] exprPairs = string.split(","); + for (String exprPair : exprPairs) { Matcher m = match(exprPair, mPattern); - if(!m.matches()) { + if (!m.matches()) { return false; } } @@ -232,11 +232,11 @@ public String getInvalidValueErrorMessage(final String string) { return "Expression pairs " + string + " is not in the format VALUE, ...>"; } } - + default Matcher match(String s, String pattern) { Pattern p = Pattern.compile(pattern); - Matcher m = p.matcher(s); - return m; + Matcher m = p.matcher(s); + return m; } } diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/IReqSymbolTable.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/IReqSymbolTable.java index 3785de49d80..caea92c0567 100644 --- a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/IReqSymbolTable.java +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/IReqSymbolTable.java @@ -39,7 +39,7 @@ import de.uni_freiburg.informatik.ultimate.core.model.models.IBoogieType; import de.uni_freiburg.informatik.ultimate.lib.pea.PhaseEventAutomata; import de.uni_freiburg.informatik.ultimate.lib.srparse.pattern.PatternType; -import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.AuxStatementContainer; +import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.AuxiliaryStatementContainer; import de.uni_freiburg.informatik.ultimate.util.datastructures.UnionFind; public interface IReqSymbolTable { @@ -67,10 +67,12 @@ public interface IReqSymbolTable { Set getClockVars(); Set getStateVars(); - + + // Allows you to easily add more elements to the Boogie program at any line without the need to create more + // interface methods. Set getAuxVars(); - - AuxStatementContainer getAuxStatementContainer(); + + AuxiliaryStatementContainer getAuxStatementContainer(); /** * Given a variable name, return the name of the primed version of this variable. diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/preferences/Pea2BoogiePreferences.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/preferences/Pea2BoogiePreferences.java index a3241088585..ef3a579ec42 100644 --- a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/preferences/Pea2BoogiePreferences.java +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/preferences/Pea2BoogiePreferences.java @@ -82,12 +82,16 @@ public class Pea2BoogiePreferences extends UltimatePreferenceInitializer { public static final String LABEL_CHECK_STATE_RECOVERABILITY = "Check state recoverability"; private static final boolean DEF_CHECK_STATE_RECOVERABILITY = true; - private static final String DESC_CHECK_STATE_RECOVERABILITY = null; - + private static final String DESC_CHECK_STATE_RECOVERABILITY = + "This setting controls whether the property check state-recoverability should be done. " + + "State-recoverability checks for the specified conditions whether it can be recovered from any location in " + + "the phase event automaton. If not, there is an error message for the specified condition."; + public static final String LABEL_STATE_RECOVERABILITY_VER_EXPR = "State recoverability expressions"; private static final String DEF_STATE_RECOVERABILITY_VER_EXPR = "ENG_READY==true, ENG_START==false"; - private static final String DESC_STATE_RECOVERABILITY_VER_STRING = "Enter the expressions for which state recoverability should be valid"; - + private static final String DESC_STATE_RECOVERABILITY_VER_STRING = + "Enter the expressions for which state recoverability should be valid"; + public static final String LABEL_GUESS_IN_OUT = "Use heuristic to find input/output definitions (if none are given)"; private static final boolean DEF_GUESS_IN_OUT = true; @@ -117,33 +121,33 @@ public Pea2BoogiePreferences() { protected UltimatePreferenceItem[] initDefaultPreferences() { return new UltimatePreferenceItem[] { - new UltimatePreferenceItem<>(LABEL_TRANSFOMER_MODE, TRANSFOMER_MODE, DESC_TRANSFOMER_MODE, - PreferenceType.Combo, PEATransformerMode.values()), - new UltimatePreferenceItem<>(LABEL_CHECK_VACUITY, DEF_CHECK_VACUITY, DESC_CHECK_VACUITY, - PreferenceType.Boolean), - new UltimatePreferenceItem<>(LABEL_CHECK_CONSISTENCY, DEF_CHECK_CONSISTENCY, DESC_CHECK_CONSISTENCY, - PreferenceType.Boolean), - new UltimatePreferenceItem<>(LABEL_CHECK_RT_INCONSISTENCY, DEF_CHECK_RT_INCONSISTENCY, - DESC_CHECK_RT_INCONSISTENCY, PreferenceType.Boolean), - new UltimatePreferenceItem<>(LABEL_USE_EPSILON, DEF_USE_EPSILON, DESC_USE_EPSILON, - PreferenceType.Boolean), - new UltimatePreferenceItem<>(LABEL_REPORT_TRIVIAL_RT_CONSISTENCY, DEF_REPORT_TRIVIAL_RT_CONSISTENCY, - DESC_REPORT_TRIVIAL_RT_CONSISTENCY, PreferenceType.Boolean), - new UltimatePreferenceItem<>(LABEL_RT_INCONSISTENCY_RANGE, DEF_RT_INCONSISTENCY_RANGE, - DESC_RT_INCONSISTENCY_RANGE, PreferenceType.Integer, - IUltimatePreferenceItemValidator.ONLY_POSITIVE), - new UltimatePreferenceItem<>(LABEL_RT_INCONSISTENCY_USE_ALL_INVARIANTS, - DEF_RT_INCONSISTENCY_USE_ALL_INVARIANTS, DESC_RT_INCONSISTENCY_USE_ALL_INVARIANTS, - PreferenceType.Boolean), - new UltimatePreferenceItem<>(LABEL_CHECK_STATE_RECOVERABILITY, DEF_CHECK_STATE_RECOVERABILITY, DESC_CHECK_STATE_RECOVERABILITY, - PreferenceType.Boolean), - new UltimatePreferenceItem<>(LABEL_STATE_RECOVERABILITY_VER_EXPR, DEF_STATE_RECOVERABILITY_VER_EXPR, - DESC_STATE_RECOVERABILITY_VER_STRING, PreferenceType.String, - IUltimatePreferenceItemValidator.EXPR_PAIR), - new UltimatePreferenceItem<>(LABEL_GUESS_IN_OUT, DEF_GUESS_IN_OUT, DESC_GUESS_IN_OUT, - PreferenceType.Boolean), - new UltimatePreferenceItem<>(LABEL_GUESS_INITIAL, DEF_GUESS_INITIAL, DESC_GUESS_INITIAL, - PreferenceType.Boolean) }; + new UltimatePreferenceItem<>(LABEL_TRANSFOMER_MODE, TRANSFOMER_MODE, DESC_TRANSFOMER_MODE, + PreferenceType.Combo, PEATransformerMode.values()), + new UltimatePreferenceItem<>(LABEL_CHECK_VACUITY, DEF_CHECK_VACUITY, DESC_CHECK_VACUITY, + PreferenceType.Boolean), + new UltimatePreferenceItem<>(LABEL_CHECK_CONSISTENCY, DEF_CHECK_CONSISTENCY, DESC_CHECK_CONSISTENCY, + PreferenceType.Boolean), + new UltimatePreferenceItem<>(LABEL_CHECK_RT_INCONSISTENCY, DEF_CHECK_RT_INCONSISTENCY, + DESC_CHECK_RT_INCONSISTENCY, PreferenceType.Boolean), + new UltimatePreferenceItem<>(LABEL_USE_EPSILON, DEF_USE_EPSILON, DESC_USE_EPSILON, + PreferenceType.Boolean), + new UltimatePreferenceItem<>(LABEL_REPORT_TRIVIAL_RT_CONSISTENCY, DEF_REPORT_TRIVIAL_RT_CONSISTENCY, + DESC_REPORT_TRIVIAL_RT_CONSISTENCY, PreferenceType.Boolean), + new UltimatePreferenceItem<>(LABEL_RT_INCONSISTENCY_RANGE, DEF_RT_INCONSISTENCY_RANGE, + DESC_RT_INCONSISTENCY_RANGE, PreferenceType.Integer, + IUltimatePreferenceItemValidator.ONLY_POSITIVE), + new UltimatePreferenceItem<>(LABEL_RT_INCONSISTENCY_USE_ALL_INVARIANTS, + DEF_RT_INCONSISTENCY_USE_ALL_INVARIANTS, DESC_RT_INCONSISTENCY_USE_ALL_INVARIANTS, + PreferenceType.Boolean), + new UltimatePreferenceItem<>(LABEL_CHECK_STATE_RECOVERABILITY, DEF_CHECK_STATE_RECOVERABILITY, + DESC_CHECK_STATE_RECOVERABILITY, PreferenceType.Boolean), + new UltimatePreferenceItem<>(LABEL_STATE_RECOVERABILITY_VER_EXPR, DEF_STATE_RECOVERABILITY_VER_EXPR, + DESC_STATE_RECOVERABILITY_VER_STRING, PreferenceType.String, + IUltimatePreferenceItemValidator.EXPR_PAIR), + new UltimatePreferenceItem<>(LABEL_GUESS_IN_OUT, DEF_GUESS_IN_OUT, DESC_GUESS_IN_OUT, + PreferenceType.Boolean), + new UltimatePreferenceItem<>(LABEL_GUESS_INITIAL, DEF_GUESS_INITIAL, DESC_GUESS_INITIAL, + PreferenceType.Boolean) }; } public static IPreferenceProvider getPreferenceProvider(final IUltimateServiceProvider services) { diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/req2pea/ReqCheckAnnotator.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/req2pea/ReqCheckAnnotator.java index 821712e2a64..41e62b5320e 100644 --- a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/req2pea/ReqCheckAnnotator.java +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/req2pea/ReqCheckAnnotator.java @@ -77,9 +77,9 @@ import de.uni_freiburg.informatik.ultimate.pea2boogie.generator.RtInconcistencyConditionGenerator.InvariantInfeasibleException; import de.uni_freiburg.informatik.ultimate.pea2boogie.preferences.Pea2BoogiePreferences; import de.uni_freiburg.informatik.ultimate.pea2boogie.results.ReqCheck; -import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.AuxStatementContainer; +import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.AuxiliaryStatementContainer; import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.PeaPhaseProgramCounter; -import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.StateRecoverabilityAuxStatement; +import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.StateRecoverabilityAuxiliaryStatement; import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.StateRecoverabilityGenerator; import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.VerificationExpression; import de.uni_freiburg.informatik.ultimate.pea2boogie.translator.CheckedReqLocation; @@ -96,6 +96,7 @@ public class ReqCheckAnnotator implements IReq2PeaAnnotator { private static final boolean DEBUG_ONLY_FIRST_NON_TRIVIAL_RT_INCONSISTENCY = false; + private static final boolean PRINT_PEA_DOT = true; private final ILogger mLogger; private final IUltimateServiceProvider mServices; @@ -194,45 +195,36 @@ private List generateAnnotations() { } private List genCheckStateRecoverability(final BoogieLocation bl) { - List list = new ArrayList<>(); - StateRecoverabilityGenerator mStRecGen = new StateRecoverabilityGenerator(); - AuxStatementContainer auxStatementContainer = mSymbolTable.getAuxStatementContainer(); - Map>> vePeaAuxStatementMap = mStRecGen.getAuxStatementPerVerificationExpression(auxStatementContainer); + List statements = new ArrayList<>(); + StateRecoverabilityGenerator stateRecoverabilityGenerator = new StateRecoverabilityGenerator(); + AuxiliaryStatementContainer auxStatementContainer = mSymbolTable.getAuxStatementContainer(); + Map>> vePeaAuxStatementMap = stateRecoverabilityGenerator.getAuxStatementPerVerificationExpression(auxStatementContainer); - for(Map.Entry>> entry : vePeaAuxStatementMap.entrySet()) { + for(Map.Entry>> entry : vePeaAuxStatementMap.entrySet()) { VerificationExpression ve = entry.getKey(); - for(Map.Entry> entryPeaStRecAuxSt : entry.getValue().entrySet()) { - Set stRecAuxStSet = entryPeaStRecAuxSt.getValue(); - for(StateRecoverabilityAuxStatement stRecAuxSt : stRecAuxStSet) { + for(Map.Entry> entryPeaStRecAuxSt : entry.getValue().entrySet()) { + Set stRecAuxStSet = entryPeaStRecAuxSt.getValue(); + for(StateRecoverabilityAuxiliaryStatement stRecAuxSt : stRecAuxStSet) { String checkLabel = "STATE_RECOVERABILITY_" + entry.getKey().getVariable() + "_" + stRecAuxSt.getPcVariable(); - Expression globalVariableTrue = mStRecGen.createExpression(bl, BoogieType.TYPE_BOOL, stRecAuxSt.getRelatedVariable(), Operator.COMPEQ, "true"); - Expression inputCondition = mStRecGen.createExpression(bl, BoogiePrimitiveType.toPrimitiveType(ve.getDataType()), ve.getVariable(), ve.getOperator(), ve.getValue()); + Expression globalVariableTrue = stateRecoverabilityGenerator.createExpression(bl, BoogieType.TYPE_BOOL, stRecAuxSt.getRelatedVariable(), Operator.COMPEQ, "true"); + Expression inputCondition = stateRecoverabilityGenerator.createExpression(bl, BoogiePrimitiveType.toPrimitiveType(ve.getDataType()), ve.getVariable(), ve.getOperator(), ve.getValue()); Expression andCondition = ExpressionFactory.newBinaryExpression(bl, Operator.LOGICAND, globalVariableTrue, inputCondition); Expression expr = ExpressionFactory.constructUnaryExpression(bl, UnaryExpression.Operator.LOGICNEG, andCondition); final ReqCheck check = createReqCheck(Spec.STATE_RECOVERABILITY, stRecAuxSt.getPeaPhasePc().getReq(), entryPeaStRecAuxSt.getKey(), String.join("", ve.getExpr())); - list.add(createAssert(expr, check, checkLabel)); + statements .add(createAssert(expr, check, checkLabel)); } } } - // DOT printen - /* - final List, PhaseEventAutomata>> counterTracePEAList = new ArrayList<>(); - for (final ReqPeas reqPea : mReqPeas) { - final PatternType pattern = reqPea.getPattern(); - - for (final Entry pea : reqPea.getCounterTrace2Pea()) { - counterTracePEAList.add(new Pair<>(pattern, pea.getValue())); - } - } - final List, PhaseEventAutomata>[]> subsets = CrossProducts.subArrays(counterTracePEAList.toArray(new Entry[counterTracePEAList.size()]), counterTracePEAList.size(), new Entry[counterTracePEAList.size()]); //Prints parallel automaton - dotPrinter(subsets); - */ - return list; + if(PRINT_PEA_DOT) { + dotPrinter(mReqPeas); + } + + return statements ; } private static List genCheckConsistency(final BoogieLocation bl) { @@ -478,7 +470,17 @@ private Expression genComparePhaseCounter(final int phaseIndex, final String pcN return ExpressionFactory.newBinaryExpression(bl, BinaryExpression.Operator.COMPEQ, identifier, intLiteral); } - private void dotPrinter(final List, PhaseEventAutomata>[]> subsets) { + private void dotPrinter(List reqPeas) { + final List, PhaseEventAutomata>> counterTracePEAList = new ArrayList<>(); + for (final ReqPeas reqPea : reqPeas) { + final PatternType pattern = reqPea.getPattern(); + + for (final Entry pea : reqPea.getCounterTrace2Pea()) { + counterTracePEAList.add(new Pair<>(pattern, pea.getValue())); + } + } + final List, PhaseEventAutomata>[]> subsets = CrossProducts.subArrays(counterTracePEAList.toArray(new Entry[counterTracePEAList.size()]), counterTracePEAList.size(), new Entry[counterTracePEAList.size()]); + for(final Entry, PhaseEventAutomata>[] subset : subsets) { final Set automataSet = Arrays.stream(subset).map(Entry, PhaseEventAutomata>::getValue).collect(Collectors.toSet()); diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/results/ReqCheck.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/results/ReqCheck.java index 73ce3a3a52f..643f1b16ff0 100644 --- a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/results/ReqCheck.java +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/results/ReqCheck.java @@ -138,13 +138,6 @@ public ReqCheck merge(final ReqCheck other) { final String message = mMessage.concat(other.getMessage()); return new ReqCheck(newSpec, startline, endline, reqIds, peaNames, message); } - - private String createMessage() { - if(mMessage == null) { - return ""; - } - return mMessage; - } public Set getReqIds() { return new LinkedHashSet<>(Arrays.asList(mReqIds)); @@ -163,7 +156,11 @@ public String toString() { if (mReqIds.length == 0) { return super.toString() + " for all requirements"; } - return super.toString() + " for " + Arrays.stream(mReqIds).collect(Collectors.joining(", ")) + " " + createMessage(); + if(mMessage.isEmpty()) { + return super.toString() + " for " + Arrays.stream(mReqIds).collect(Collectors.joining(", ")); + } else { + return super.toString() + " for " + Arrays.stream(mReqIds).collect(Collectors.joining(", ")) + " " + mMessage; + } } @Override @@ -202,7 +199,7 @@ public boolean equals(final Object obj) { if (!Arrays.equals(mPeaNames, other.mPeaNames)) { return false; } - if(!mMessage.equalsIgnoreCase(other.getMessage())) { + if(!mMessage.equals(other.getMessage())) { return false; } return true; diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/results/ReqCheckStateRecoverabilityResult.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/results/ReqCheckStateRecoverabilityResult.java index 60dfcb766df..f84796c2ebc 100644 --- a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/results/ReqCheckStateRecoverabilityResult.java +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/results/ReqCheckStateRecoverabilityResult.java @@ -5,7 +5,7 @@ import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.structure.IAction; import de.uni_freiburg.informatik.ultimate.util.CoreUtil; -public class ReqCheckStateRecoverabilityResult extends ReqCheckFailResult { +public class ReqCheckStateRecoverabilityResult extends ReqCheckFailResult{ private final String mMessage; diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/AuxStatement.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/AuxiliaryStatement.java similarity index 73% rename from trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/AuxStatement.java rename to trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/AuxiliaryStatement.java index 1094aa0b168..2bf5dd218ba 100644 --- a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/AuxStatement.java +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/AuxiliaryStatement.java @@ -5,11 +5,11 @@ import de.uni_freiburg.informatik.ultimate.boogie.BoogieLocation; import de.uni_freiburg.informatik.ultimate.boogie.ast.Statement; -import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.AuxStatementContainer.StRecExpr; +import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.AuxiliaryStatementContainer.StatementAssignment; -public interface AuxStatement { +public interface AuxiliaryStatement { - public Statement getStatement(StRecExpr stRecExpr); + public Statement getStatement(StatementAssignment stRecExpr); public BoogieLocation setBoogieLocation(BoogieLocation loc); diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/AuxStatementContainer.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/AuxiliaryStatementContainer.java similarity index 57% rename from trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/AuxStatementContainer.java rename to trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/AuxiliaryStatementContainer.java index da31df7392c..0040eeda5c2 100644 --- a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/AuxStatementContainer.java +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/AuxiliaryStatementContainer.java @@ -9,27 +9,27 @@ import de.uni_freiburg.informatik.ultimate.boogie.BoogieLocation; import de.uni_freiburg.informatik.ultimate.boogie.ast.Statement; -import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.AuxStatementContainer.StRecExpr; +import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.AuxiliaryStatementContainer.StatementAssignment; -public class AuxStatementContainer { - public enum StRecExpr { +public class AuxiliaryStatementContainer { + public enum StatementAssignment { DECL_VAR, ASSIGN_VAR, IF_ST; } - private Map sreMap; + private Map mStatementMap; private Set statements; - public AuxStatementContainer() { - sreMap = new HashMap<>(); + public AuxiliaryStatementContainer() { + mStatementMap = new HashMap<>(); } - public AuxStatementContainer(AuxStatementContainer auxStatement) { - sreMap = auxStatement.getSreMap(); + public AuxiliaryStatementContainer(AuxiliaryStatementContainer auxStatement) { + mStatementMap = auxStatement.getSreMap(); } - public List getStatements(StRecExpr stRecExpr) { + public List getStatements(StatementAssignment stRecExpr) { List statList = new ArrayList<>(); - for(AuxStatement auxStatement : sreMap.values()) { + for(AuxiliaryStatement auxStatement : mStatementMap.values()) { Statement s = auxStatement.getStatement(stRecExpr); if(s != null) { statList.add(s); @@ -40,7 +40,7 @@ public List getStatements(StRecExpr stRecExpr) { public Set getRelatedVariableForInstance(Object object) { Set relatedVariables = new HashSet<>(); - for(Map.Entry entry : sreMap.entrySet()) { + for(Map.Entry entry : mStatementMap.entrySet()) { if(entry.getValue().getClass().getName().equals(object.getClass().getName())) { relatedVariables.add(entry.getKey()); } @@ -48,9 +48,9 @@ public Set getRelatedVariableForInstance(Object object) { return relatedVariables; } - public Set setBoogieLocationForInstance(Object object, StRecExpr stRecExpr, final BoogieLocation bl) { + public Set setBoogieLocationForInstance(Object object, StatementAssignment stRecExpr, final BoogieLocation bl) { Set statements = new HashSet<>(); - for(Map.Entry entry : sreMap.entrySet()) { + for(Map.Entry entry : mStatementMap.entrySet()) { if(entry.getValue().getClass().getName().equals(object.getClass().getName())) { Statement statement = entry.getValue().getStatement(stRecExpr); if(statement != null) { @@ -62,20 +62,20 @@ public Set setBoogieLocationForInstance(Object object, StRecExpr stRe return statements; } - public AuxStatement addAuxStatement(String variable, AuxStatement auxStatement) { - if(sreMap == null) { - sreMap = new HashMap<>(); + public AuxiliaryStatement addAuxStatement(String variable, AuxiliaryStatement auxStatement) { + if(mStatementMap == null) { + mStatementMap = new HashMap<>(); } - sreMap.put(variable, auxStatement); + mStatementMap.put(variable, auxStatement); return auxStatement; } - public Map getSreMap() { - return sreMap; + public Map getSreMap() { + return mStatementMap; } - public void setSreMap(Map sreMap) { - this.sreMap = sreMap; + public void setSreMap(Map sreMap) { + this.mStatementMap = sreMap; } public Set getStatements() { diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/StateRecoverabilityAuxStatement.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/StateRecoverabilityAuxiliaryStatement.java similarity index 85% rename from trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/StateRecoverabilityAuxStatement.java rename to trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/StateRecoverabilityAuxiliaryStatement.java index c443bb8e051..7ecfe7e1ce5 100644 --- a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/StateRecoverabilityAuxStatement.java +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/StateRecoverabilityAuxiliaryStatement.java @@ -5,9 +5,9 @@ import de.uni_freiburg.informatik.ultimate.boogie.BoogieLocation; import de.uni_freiburg.informatik.ultimate.boogie.ast.Statement; -import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.AuxStatementContainer.StRecExpr; +import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.AuxiliaryStatementContainer.StatementAssignment; -public class StateRecoverabilityAuxStatement implements AuxStatement { +public class StateRecoverabilityAuxiliaryStatement implements AuxiliaryStatement { private PeaPhaseProgramCounter peaPhasePc; private String relatedVariable; @@ -19,11 +19,11 @@ public class StateRecoverabilityAuxStatement implements AuxStatement { private Statement assignVar; private Statement ifSt; - public StateRecoverabilityAuxStatement(String variable) { + public StateRecoverabilityAuxiliaryStatement(String variable) { this.relatedVariable = variable; } - public StateRecoverabilityAuxStatement(PeaPhaseProgramCounter peaPhasePc, String variable, String pcVariable, int pc, VerificationExpression ve) { + public StateRecoverabilityAuxiliaryStatement(PeaPhaseProgramCounter peaPhasePc, String variable, String pcVariable, int pc, VerificationExpression ve) { this.peaPhasePc = peaPhasePc; this.relatedVariable = variable; this.pcVariable = pcVariable; @@ -32,7 +32,7 @@ public StateRecoverabilityAuxStatement(PeaPhaseProgramCounter peaPhasePc, String } @Override - public Statement getStatement(StRecExpr stRecExpr) { + public Statement getStatement(StatementAssignment stRecExpr) { Statement s = null; switch (stRecExpr) { case DECL_VAR: diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/StateRecoverabilityGenerator.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/StateRecoverabilityGenerator.java index 795bee8b9f4..69fb53f7e0b 100644 --- a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/StateRecoverabilityGenerator.java +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/StateRecoverabilityGenerator.java @@ -280,22 +280,22 @@ private static Script buildSolver(final IUltimateServiceProvider services) throw return SolverBuilder.buildAndInitializeSolver(services, settings, "RtInconsistencySolver"); } - public Map>> - getAuxStatementPerVerificationExpression(AuxStatementContainer auxStatementContainer) { - Map>> vePeaAuxStatementMap = + public Map>> + getAuxStatementPerVerificationExpression(AuxiliaryStatementContainer auxStatementContainer) { + Map>> vePeaAuxStatementMap = new HashMap<>(); - for (AuxStatement auxStatement : auxStatementContainer.getSreMap().values()) { - if (auxStatement instanceof StateRecoverabilityAuxStatement) { - StateRecoverabilityAuxStatement stRecAuxSt = (StateRecoverabilityAuxStatement) auxStatement; + for (AuxiliaryStatement auxStatement : auxStatementContainer.getSreMap().values()) { + if (auxStatement instanceof StateRecoverabilityAuxiliaryStatement) { + StateRecoverabilityAuxiliaryStatement stRecAuxSt = (StateRecoverabilityAuxiliaryStatement) auxStatement; if (!vePeaAuxStatementMap.containsKey(stRecAuxSt.getVerificationExpression())) { vePeaAuxStatementMap.put(stRecAuxSt.getVerificationExpression(), new HashMap<>()); } - Map> peaAuxStatementMap = + Map> peaAuxStatementMap = vePeaAuxStatementMap.get(stRecAuxSt.getVerificationExpression()); if (!peaAuxStatementMap.containsKey(stRecAuxSt.getPeaPhasePc().getPea())) { peaAuxStatementMap.put(stRecAuxSt.getPeaPhasePc().getPea(), new HashSet<>()); } - Set stRecAuxStSet = + Set stRecAuxStSet = peaAuxStatementMap.get(stRecAuxSt.getPeaPhasePc().getPea()); stRecAuxStSet.add(stRecAuxSt); } diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/testgen/Req2ModifySymbolTablePea.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/testgen/Req2ModifySymbolTablePea.java index a10ddc5172f..83f95b38cc1 100644 --- a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/testgen/Req2ModifySymbolTablePea.java +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/testgen/Req2ModifySymbolTablePea.java @@ -51,9 +51,9 @@ import de.uni_freiburg.informatik.ultimate.pea2boogie.req2pea.ReqCheckAnnotator; import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.VerificationExpression; import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.VerificationExpressionContainer; -import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.AuxStatement; +import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.AuxiliaryStatement; import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.PeaPhaseProgramCounter; -import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.StateRecoverabilityAuxStatement; +import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.StateRecoverabilityAuxiliaryStatement; import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.StateRecoverabilityGenerator; import de.uni_freiburg.informatik.ultimate.pea2boogie.translator.ReqSymboltableBuilder; import de.uni_freiburg.informatik.ultimate.pea2boogie.translator.ReqSymboltableBuilder.ErrorInfo; @@ -125,7 +125,7 @@ public void transform(IReq2Pea req2pea) { //Necessary in Transformer since otherwise unused global variables would be in the Boogie code Map> veLocationMap = stRecGen.getRelevantLocationsFromPea(simplePeas, vec); - List sreList = createGlobalVariableForVerificationExpression(builder, veLocationMap, vec); + List sreList = createGlobalVariableForVerificationExpression(builder, veLocationMap, vec); //Creating the statements createAssignBoolToGlobalVariableBeforeWhileLoop(sreList); @@ -134,10 +134,10 @@ public void transform(IReq2Pea req2pea) { mSymbolTable = builder.constructSymbolTable(); } - private void createIfStatementInWhileLoop(List auxStatements) { - for(AuxStatement auxStatement : auxStatements) { - if(auxStatement instanceof StateRecoverabilityAuxStatement) { - StateRecoverabilityAuxStatement auxStatementStRec = (StateRecoverabilityAuxStatement) auxStatement; + private void createIfStatementInWhileLoop(List auxStatements) { + for(AuxiliaryStatement auxStatement : auxStatements) { + if(auxStatement instanceof StateRecoverabilityAuxiliaryStatement) { + StateRecoverabilityAuxiliaryStatement auxStatementStRec = (StateRecoverabilityAuxiliaryStatement) auxStatement; VerificationExpression ve = auxStatementStRec.getVerificationExpression(); ILocation loc = auxStatementStRec.getBoogieLocation(); // Create expression @@ -163,8 +163,8 @@ private VerificationExpressionContainer getVerificationExpression(IReq2Pea req2p return vec; } - private List createGlobalVariableForVerificationExpression(ReqSymboltableBuilder builder, Map> veLocationMaptionMap, VerificationExpressionContainer vec) { - List sreList = new ArrayList<>(); + private List createGlobalVariableForVerificationExpression(ReqSymboltableBuilder builder, Map> veLocationMaptionMap, VerificationExpressionContainer vec) { + List sreList = new ArrayList<>(); for(Map.Entry> entry : veLocationMaptionMap.entrySet()) { for(PeaPhaseProgramCounter peaPhasePc : entry.getValue()) { String pcName = getPcName(peaPhasePc.getPea().getName()); @@ -173,7 +173,7 @@ private List createGlobalVariableForVerificationExpression(ReqSymb String variable = entry.getKey().getVariable(); String dataType = entry.getKey().getDataType(); String globalVariable = pcName + pc + "_StRec_" + variable; - StateRecoverabilityAuxStatement auxStatement = new StateRecoverabilityAuxStatement(peaPhasePc, globalVariable, pcName, pc, entry.getKey()); + StateRecoverabilityAuxiliaryStatement auxStatement = new StateRecoverabilityAuxiliaryStatement(peaPhasePc, globalVariable, pcName, pc, entry.getKey()); sreList.add(builder.addAuxVar(auxStatement, globalVariable, "bool", null)); } @@ -181,10 +181,10 @@ private List createGlobalVariableForVerificationExpression(ReqSymb return sreList; } - private void createAssignBoolToGlobalVariableBeforeWhileLoop(List auxStatements) { - for(AuxStatement auxStatement : auxStatements) { - if(auxStatement instanceof StateRecoverabilityAuxStatement) { - StateRecoverabilityAuxStatement auxStatementStateRecoverability = (StateRecoverabilityAuxStatement) auxStatement; + private void createAssignBoolToGlobalVariableBeforeWhileLoop(List auxStatements) { + for(AuxiliaryStatement auxStatement : auxStatements) { + if(auxStatement instanceof StateRecoverabilityAuxiliaryStatement) { + StateRecoverabilityAuxiliaryStatement auxStatementStateRecoverability = (StateRecoverabilityAuxiliaryStatement) auxStatement; BooleanLiteral booleanLiteral = ExpressionFactory.createBooleanLiteral(null, false); AssignmentStatement assignmentStatement = genAssignmentStmt(constructNewLocation(), auxStatementStateRecoverability.getRelatedVariable(), booleanLiteral); auxStatementStateRecoverability.setAssignVar(assignmentStatement); diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/translator/Req2BoogieTranslator.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/translator/Req2BoogieTranslator.java index 57c252f7f7d..ddd605e56f6 100644 --- a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/translator/Req2BoogieTranslator.java +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/translator/Req2BoogieTranslator.java @@ -84,8 +84,8 @@ import de.uni_freiburg.informatik.ultimate.pea2boogie.req2pea.IReq2PeaAnnotator; import de.uni_freiburg.informatik.ultimate.pea2boogie.req2pea.IReq2PeaTransformer; import de.uni_freiburg.informatik.ultimate.pea2boogie.req2pea.Req2Pea; -import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.StateRecoverabilityAuxStatement; -import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.AuxStatementContainer.StRecExpr; +import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.StateRecoverabilityAuxiliaryStatement; +import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.AuxiliaryStatementContainer.StatementAssignment; import de.uni_freiburg.informatik.ultimate.pea2boogie.testgen.ReqInOutGuesser; import de.uni_freiburg.informatik.ultimate.util.simplifier.NormalFormTransformer; @@ -560,7 +560,7 @@ private Statement[] genWhileLoopBody(final BoogieLocation bl) { } } // Assign St-Recoverability if statement - stmtList.addAll(mSymboltable.getAuxStatementContainer().getStatements(StRecExpr.IF_ST)); + stmtList.addAll(mSymboltable.getAuxStatementContainer().getStatements(StatementAssignment.IF_ST)); stmtList.addAll(mReqCheckAnnotator.getStateChecks()); stmtList.addAll( mSymboltable.getPcVars().stream().map(this::genStateVarAssignHistory).collect(Collectors.toList())); @@ -665,7 +665,7 @@ private Statement[] generateProcedureBody(final BoogieLocation bl, final List init) { modifiedVarsList.addAll(mSymboltable.getHistoryVars()); modifiedVarsList.addAll(mSymboltable.getEventVars()); // Adds only instance of class type StateRecoverabilityAuxStatement - modifiedVarsList.addAll(mSymboltable.getAuxStatementContainer().getRelatedVariableForInstance(new StateRecoverabilityAuxStatement(""))); + modifiedVarsList.addAll(mSymboltable.getAuxStatementContainer().getRelatedVariableForInstance(new StateRecoverabilityAuxiliaryStatement(""))); final VariableLHS[] modifiedVars = new VariableLHS[modifiedVarsList.size()]; for (int i = 0; i < modifiedVars.length; i++) { diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/translator/ReqSymboltableBuilder.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/translator/ReqSymboltableBuilder.java index 248c1e892c7..18c2ddc70ac 100644 --- a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/translator/ReqSymboltableBuilder.java +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/translator/ReqSymboltableBuilder.java @@ -67,8 +67,8 @@ import de.uni_freiburg.informatik.ultimate.lib.srparse.pattern.DeclarationPattern.VariableCategory; import de.uni_freiburg.informatik.ultimate.lib.srparse.pattern.PatternType; import de.uni_freiburg.informatik.ultimate.pea2boogie.IReqSymbolTable; -import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.AuxStatement; -import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.AuxStatementContainer; +import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.AuxiliaryStatement; +import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.AuxiliaryStatementContainer; import de.uni_freiburg.informatik.ultimate.util.datastructures.UnionFind; import de.uni_freiburg.informatik.ultimate.util.datastructures.relation.LinkedHashRelation; @@ -87,7 +87,7 @@ public class ReqSymboltableBuilder { private final Map mId2IdExpr; private final Map mId2VarLHS; - private final AuxStatementContainer mAuxStatements; + private final AuxiliaryStatementContainer mAuxStatements; private final Set mAuxVars; private final Set mStateVars; private final Set mConstVars; @@ -113,7 +113,7 @@ public ReqSymboltableBuilder(final ILogger logger) { mId2IdExpr = new LinkedHashMap<>(); mId2VarLHS = new LinkedHashMap<>(); - mAuxStatements = new AuxStatementContainer(); + mAuxStatements = new AuxiliaryStatementContainer(); mAuxVars = new LinkedHashSet<>(); mStateVars = new LinkedHashSet<>(); mConstVars = new LinkedHashSet<>(); @@ -296,7 +296,7 @@ private void addVar(final String name, final BoogieType type, final PatternType< addVarOneKind(getPrimedVarId(name), type, source, mPrimedVars); } - public AuxStatement addAuxVar(final AuxStatement auxStatement, final String name, final String boogieType, final PatternType source) { + public AuxiliaryStatement addAuxVar(final AuxiliaryStatement auxStatement, final String name, final String boogieType, final PatternType source) { Set kind = mAuxVars; auxStatement.setBoogieLocation(DUMMY_LOC); switch (boogieType.toLowerCase()) { @@ -407,7 +407,7 @@ private static final class ReqSymbolTable implements IReqSymbolTable { private final Map mConst2Value; private final Map, BoogieLocation> mReq2Loc; - private final AuxStatementContainer mAuxStatements; + private final AuxiliaryStatementContainer mAuxStatements; private final Set mAuxVars; private final Set mStateVars; private final Set mConstVars; @@ -423,7 +423,7 @@ private static final class ReqSymbolTable implements IReqSymbolTable { private final UnionFind mEquivalences; private ReqSymbolTable(final String deltaVar, final Map id2Type, - final Map id2idExp, final Map id2VarLhs, final AuxStatementContainer auxStatements, + final Map id2idExp, final Map id2VarLhs, final AuxiliaryStatementContainer auxStatements, final Set auxVars, Set stateVars, final Set primedVars, final Set historyVars, final Set constVars, final Set eventVars, final Set pcVars, final Set clockVars, final Map, BoogieLocation> req2loc, @@ -537,7 +537,7 @@ public Set getAuxVars() { } @Override - public AuxStatementContainer getAuxStatementContainer( ) { + public AuxiliaryStatementContainer getAuxStatementContainer( ) { return mAuxStatements; } diff --git a/trunk/source/ReqToTest/src/de/uni_freiburg/informatik/ultimate/reqtotest/req/Req2TestReqSymbolTable.java b/trunk/source/ReqToTest/src/de/uni_freiburg/informatik/ultimate/reqtotest/req/Req2TestReqSymbolTable.java index 6812a739f0e..edc100b98bd 100644 --- a/trunk/source/ReqToTest/src/de/uni_freiburg/informatik/ultimate/reqtotest/req/Req2TestReqSymbolTable.java +++ b/trunk/source/ReqToTest/src/de/uni_freiburg/informatik/ultimate/reqtotest/req/Req2TestReqSymbolTable.java @@ -37,7 +37,7 @@ import de.uni_freiburg.informatik.ultimate.logic.FunctionSymbol; import de.uni_freiburg.informatik.ultimate.logic.TermVariable; import de.uni_freiburg.informatik.ultimate.pea2boogie.IReqSymbolTable; -import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.AuxStatementContainer; +import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.AuxiliaryStatementContainer; import de.uni_freiburg.informatik.ultimate.reqtotest.graphtransformer.FakeBoogieVar; import de.uni_freiburg.informatik.ultimate.util.datastructures.UnionFind; @@ -371,7 +371,7 @@ public Set getAuxVars() { } @Override - public AuxStatementContainer getAuxStatementContainer() { + public AuxiliaryStatementContainer getAuxStatementContainer() { // TODO Auto-generated method stub return null; } From 76c11702b379b8ac95743b45292f14a208a95660 Mon Sep 17 00:00:00 2001 From: Tobias Wiessner Date: Mon, 28 Aug 2023 17:37:27 +0200 Subject: [PATCH 13/23] Review fix --- .../ReqCheckStateRecoverabilityResult.java | 32 +++++++++++++++++++ .../AuxiliaryStatement.java | 32 +++++++++++++++++++ .../AuxiliaryStatementContainer.java | 32 +++++++++++++++++++ .../PeaPhaseProgramCounter.java | 32 +++++++++++++++++++ ...StateRecoverabilityAuxiliaryStatement.java | 32 +++++++++++++++++++ .../StateRecoverabilityGenerator.java | 32 +++++++++++++++++++ .../VerificationExpression.java | 32 +++++++++++++++++++ .../VerificationExpressionContainer.java | 32 +++++++++++++++++++ 8 files changed, 256 insertions(+) diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/results/ReqCheckStateRecoverabilityResult.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/results/ReqCheckStateRecoverabilityResult.java index f84796c2ebc..9615f953903 100644 --- a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/results/ReqCheckStateRecoverabilityResult.java +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/results/ReqCheckStateRecoverabilityResult.java @@ -1,3 +1,29 @@ +/* + * Copyright (C) 2023 Tobias Wießner + * Copyright (C) 2023 University of Freiburg + * + * This file is part of the ULTIMATE PEAtoBoogie plug-in. + * + * The ULTIMATE PEAtoBoogie plug-in is free software: you can redistribute it and/or modify + * it under the terms of the GNU Lesser General Public License as published + * by the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * The ULTIMATE PEAtoBoogie plug-in is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU Lesser General Public License for more details. + * + * You should have received a copy of the GNU Lesser General Public License + * along with the ULTIMATE PEAtoBoogie plug-in. If not, see . + * + * Additional permission under GNU GPL version 3 section 7: + * If you modify the ULTIMATE PEAtoBoogie plug-in, or any covered work, by linking + * or combining it with Eclipse RCP (or a modified version of Eclipse RCP), + * containing parts covered by the terms of the Eclipse Public License, the + * licensors of the ULTIMATE PEAtoBoogie plug-in grant you additional permission + * to convey the resulting work. + */ package de.uni_freiburg.informatik.ultimate.pea2boogie.results; import de.uni_freiburg.informatik.ultimate.core.model.models.IElement; @@ -5,6 +31,12 @@ import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.structure.IAction; import de.uni_freiburg.informatik.ultimate.util.CoreUtil; +/** +* +* @author Tobias Wießner +* +*/ + public class ReqCheckStateRecoverabilityResult extends ReqCheckFailResult{ private final String mMessage; diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/AuxiliaryStatement.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/AuxiliaryStatement.java index 2bf5dd218ba..f7211217002 100644 --- a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/AuxiliaryStatement.java +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/AuxiliaryStatement.java @@ -1,3 +1,29 @@ +/* + * Copyright (C) 2023 Tobias Wießner + * Copyright (C) 2023 University of Freiburg + * + * This file is part of the ULTIMATE PEAtoBoogie plug-in. + * + * The ULTIMATE PEAtoBoogie plug-in is free software: you can redistribute it and/or modify + * it under the terms of the GNU Lesser General Public License as published + * by the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * The ULTIMATE PEAtoBoogie plug-in is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU Lesser General Public License for more details. + * + * You should have received a copy of the GNU Lesser General Public License + * along with the ULTIMATE PEAtoBoogie plug-in. If not, see . + * + * Additional permission under GNU GPL version 3 section 7: + * If you modify the ULTIMATE PEAtoBoogie plug-in, or any covered work, by linking + * or combining it with Eclipse RCP (or a modified version of Eclipse RCP), + * containing parts covered by the terms of the Eclipse Public License, the + * licensors of the ULTIMATE PEAtoBoogie plug-in grant you additional permission + * to convey the resulting work. + */ package de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability; import java.util.ArrayList; @@ -7,6 +33,12 @@ import de.uni_freiburg.informatik.ultimate.boogie.ast.Statement; import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.AuxiliaryStatementContainer.StatementAssignment; +/** +* +* @author Tobias Wießner +* +*/ + public interface AuxiliaryStatement { public Statement getStatement(StatementAssignment stRecExpr); diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/AuxiliaryStatementContainer.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/AuxiliaryStatementContainer.java index 0040eeda5c2..2e79702125f 100644 --- a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/AuxiliaryStatementContainer.java +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/AuxiliaryStatementContainer.java @@ -1,3 +1,29 @@ +/* + * Copyright (C) 2023 Tobias Wießner + * Copyright (C) 2023 University of Freiburg + * + * This file is part of the ULTIMATE PEAtoBoogie plug-in. + * + * The ULTIMATE PEAtoBoogie plug-in is free software: you can redistribute it and/or modify + * it under the terms of the GNU Lesser General Public License as published + * by the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * The ULTIMATE PEAtoBoogie plug-in is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU Lesser General Public License for more details. + * + * You should have received a copy of the GNU Lesser General Public License + * along with the ULTIMATE PEAtoBoogie plug-in. If not, see . + * + * Additional permission under GNU GPL version 3 section 7: + * If you modify the ULTIMATE PEAtoBoogie plug-in, or any covered work, by linking + * or combining it with Eclipse RCP (or a modified version of Eclipse RCP), + * containing parts covered by the terms of the Eclipse Public License, the + * licensors of the ULTIMATE PEAtoBoogie plug-in grant you additional permission + * to convey the resulting work. + */ package de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability; import java.util.ArrayList; @@ -11,6 +37,12 @@ import de.uni_freiburg.informatik.ultimate.boogie.ast.Statement; import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.AuxiliaryStatementContainer.StatementAssignment; +/** +* +* @author Tobias Wießner +* +*/ + public class AuxiliaryStatementContainer { public enum StatementAssignment { DECL_VAR, ASSIGN_VAR, IF_ST; diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/PeaPhaseProgramCounter.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/PeaPhaseProgramCounter.java index c1d2d481a49..8fe05afa59d 100644 --- a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/PeaPhaseProgramCounter.java +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/PeaPhaseProgramCounter.java @@ -1,3 +1,29 @@ +/* + * Copyright (C) 2023 Tobias Wießner + * Copyright (C) 2023 University of Freiburg + * + * This file is part of the ULTIMATE PEAtoBoogie plug-in. + * + * The ULTIMATE PEAtoBoogie plug-in is free software: you can redistribute it and/or modify + * it under the terms of the GNU Lesser General Public License as published + * by the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * The ULTIMATE PEAtoBoogie plug-in is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU Lesser General Public License for more details. + * + * You should have received a copy of the GNU Lesser General Public License + * along with the ULTIMATE PEAtoBoogie plug-in. If not, see . + * + * Additional permission under GNU GPL version 3 section 7: + * If you modify the ULTIMATE PEAtoBoogie plug-in, or any covered work, by linking + * or combining it with Eclipse RCP (or a modified version of Eclipse RCP), + * containing parts covered by the terms of the Eclipse Public License, the + * licensors of the ULTIMATE PEAtoBoogie plug-in grant you additional permission + * to convey the resulting work. + */ package de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability; import java.util.Collection; @@ -9,6 +35,12 @@ import de.uni_freiburg.informatik.ultimate.lib.pea.PhaseEventAutomata; import de.uni_freiburg.informatik.ultimate.lib.srparse.pattern.PatternType; +/** +* +* @author Tobias Wießner +* +*/ + public class PeaPhaseProgramCounter { private final int pc; diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/StateRecoverabilityAuxiliaryStatement.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/StateRecoverabilityAuxiliaryStatement.java index 7ecfe7e1ce5..f21fc98926d 100644 --- a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/StateRecoverabilityAuxiliaryStatement.java +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/StateRecoverabilityAuxiliaryStatement.java @@ -1,3 +1,29 @@ +/* + * Copyright (C) 2023 Tobias Wießner + * Copyright (C) 2023 University of Freiburg + * + * This file is part of the ULTIMATE PEAtoBoogie plug-in. + * + * The ULTIMATE PEAtoBoogie plug-in is free software: you can redistribute it and/or modify + * it under the terms of the GNU Lesser General Public License as published + * by the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * The ULTIMATE PEAtoBoogie plug-in is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU Lesser General Public License for more details. + * + * You should have received a copy of the GNU Lesser General Public License + * along with the ULTIMATE PEAtoBoogie plug-in. If not, see . + * + * Additional permission under GNU GPL version 3 section 7: + * If you modify the ULTIMATE PEAtoBoogie plug-in, or any covered work, by linking + * or combining it with Eclipse RCP (or a modified version of Eclipse RCP), + * containing parts covered by the terms of the Eclipse Public License, the + * licensors of the ULTIMATE PEAtoBoogie plug-in grant you additional permission + * to convey the resulting work. + */ package de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability; import java.util.ArrayList; @@ -7,6 +33,12 @@ import de.uni_freiburg.informatik.ultimate.boogie.ast.Statement; import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.AuxiliaryStatementContainer.StatementAssignment; +/** +* +* @author Tobias Wießner +* +*/ + public class StateRecoverabilityAuxiliaryStatement implements AuxiliaryStatement { private PeaPhaseProgramCounter peaPhasePc; diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/StateRecoverabilityGenerator.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/StateRecoverabilityGenerator.java index 69fb53f7e0b..c582b1068eb 100644 --- a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/StateRecoverabilityGenerator.java +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/StateRecoverabilityGenerator.java @@ -1,3 +1,29 @@ +/* + * Copyright (C) 2023 Tobias Wießner + * Copyright (C) 2023 University of Freiburg + * + * This file is part of the ULTIMATE PEAtoBoogie plug-in. + * + * The ULTIMATE PEAtoBoogie plug-in is free software: you can redistribute it and/or modify + * it under the terms of the GNU Lesser General Public License as published + * by the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * The ULTIMATE PEAtoBoogie plug-in is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU Lesser General Public License for more details. + * + * You should have received a copy of the GNU Lesser General Public License + * along with the ULTIMATE PEAtoBoogie plug-in. If not, see . + * + * Additional permission under GNU GPL version 3 section 7: + * If you modify the ULTIMATE PEAtoBoogie plug-in, or any covered work, by linking + * or combining it with Eclipse RCP (or a modified version of Eclipse RCP), + * containing parts covered by the terms of the Eclipse Public License, the + * licensors of the ULTIMATE PEAtoBoogie plug-in grant you additional permission + * to convey the resulting work. + */ package de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability; import java.util.ArrayList; @@ -62,6 +88,12 @@ import de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTInterpol; import de.uni_freiburg.informatik.ultimate.util.ConstructionCache; +/** +* +* @author Tobias Wießner +* +*/ + public class StateRecoverabilityGenerator { private IReqSymbolTable mReqSymboltable; diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/VerificationExpression.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/VerificationExpression.java index 6c169a80876..413da3a414c 100644 --- a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/VerificationExpression.java +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/VerificationExpression.java @@ -1,9 +1,41 @@ +/* + * Copyright (C) 2023 Tobias Wießner + * Copyright (C) 2023 University of Freiburg + * + * This file is part of the ULTIMATE PEAtoBoogie plug-in. + * + * The ULTIMATE PEAtoBoogie plug-in is free software: you can redistribute it and/or modify + * it under the terms of the GNU Lesser General Public License as published + * by the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * The ULTIMATE PEAtoBoogie plug-in is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU Lesser General Public License for more details. + * + * You should have received a copy of the GNU Lesser General Public License + * along with the ULTIMATE PEAtoBoogie plug-in. If not, see . + * + * Additional permission under GNU GPL version 3 section 7: + * If you modify the ULTIMATE PEAtoBoogie plug-in, or any covered work, by linking + * or combining it with Eclipse RCP (or a modified version of Eclipse RCP), + * containing parts covered by the terms of the Eclipse Public License, the + * licensors of the ULTIMATE PEAtoBoogie plug-in grant you additional permission + * to convey the resulting work. + */ package de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability; import javax.management.RuntimeErrorException; import de.uni_freiburg.informatik.ultimate.boogie.type.BoogiePrimitiveType; +/** +* +* @author Tobias Wießner +* +*/ + public class VerificationExpression { private final String[] expr; private final String dataType; diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/VerificationExpressionContainer.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/VerificationExpressionContainer.java index 88e6b56d9d7..c9ca397277d 100644 --- a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/VerificationExpressionContainer.java +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/VerificationExpressionContainer.java @@ -1,3 +1,29 @@ +/* + * Copyright (C) 2023 Tobias Wießner + * Copyright (C) 2023 University of Freiburg + * + * This file is part of the ULTIMATE PEAtoBoogie plug-in. + * + * The ULTIMATE PEAtoBoogie plug-in is free software: you can redistribute it and/or modify + * it under the terms of the GNU Lesser General Public License as published + * by the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * The ULTIMATE PEAtoBoogie plug-in is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU Lesser General Public License for more details. + * + * You should have received a copy of the GNU Lesser General Public License + * along with the ULTIMATE PEAtoBoogie plug-in. If not, see . + * + * Additional permission under GNU GPL version 3 section 7: + * If you modify the ULTIMATE PEAtoBoogie plug-in, or any covered work, by linking + * or combining it with Eclipse RCP (or a modified version of Eclipse RCP), + * containing parts covered by the terms of the Eclipse Public License, the + * licensors of the ULTIMATE PEAtoBoogie plug-in grant you additional permission + * to convey the resulting work. + */ package de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability; import java.util.ArrayList; @@ -15,6 +41,12 @@ import de.uni_freiburg.informatik.ultimate.lib.srparse.pattern.PatternType.ReqPeas; import de.uni_freiburg.informatik.ultimate.pea2boogie.req2pea.IReq2Pea; +/** +* +* @author Tobias Wießner +* +*/ + public class VerificationExpressionContainer { // Pattern for input expression From d9cf93ca15775a74602bcf8d025b2ba623bcb1b5 Mon Sep 17 00:00:00 2001 From: Tobias Wiessner Date: Mon, 28 Aug 2023 17:46:29 +0200 Subject: [PATCH 14/23] Review fix --- .../pea2boogie/staterecoverability/AuxiliaryStatement.java | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/AuxiliaryStatement.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/AuxiliaryStatement.java index f7211217002..db1844b0473 100644 --- a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/AuxiliaryStatement.java +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/AuxiliaryStatement.java @@ -31,10 +31,15 @@ import de.uni_freiburg.informatik.ultimate.boogie.BoogieLocation; import de.uni_freiburg.informatik.ultimate.boogie.ast.Statement; +import de.uni_freiburg.informatik.ultimate.lib.pea.PhaseEventAutomata; +import de.uni_freiburg.informatik.ultimate.pea2boogie.IReqSymbolTable; +import de.uni_freiburg.informatik.ultimate.pea2boogie.req2pea.IReq2Pea; import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.AuxiliaryStatementContainer.StatementAssignment; /** * +* Interface for a class containing a statement to be inserted at a certain line in the Boogie program. +* * @author Tobias Wießner * */ From 661a8b78729d58c3fd4a67cfd860f5d52824a843 Mon Sep 17 00:00:00 2001 From: Tobias Wiessner Date: Tue, 29 Aug 2023 17:05:36 +0200 Subject: [PATCH 15/23] Review fix --- .../ultimate/boogie/ExpressionFactory.java | 9 +- .../ultimate/boogie/ast/IfThenExpression.java | 120 ++++++++++++++++++ .../boogie/typechecker/TypeCheckHelper.java | 17 +++ .../pea2boogie/PEAtoBoogieObserver.java | 2 + .../pea2boogie/req2pea/ReqCheckAnnotator.java | 8 +- ...StateRecoverabilityAuxiliaryStatement.java | 8 +- .../StateRecoverabilityGenerator.java | 12 +- ...eRecoverabilityVerificationCondition.java} | 119 +++++++++-------- ...bilityVerificationConditionContainer.java} | 20 +-- .../testgen/Req2ModifySymbolTablePea.java | 18 +-- 10 files changed, 241 insertions(+), 92 deletions(-) create mode 100644 trunk/source/Library-BoogieAST/src/de/uni_freiburg/informatik/ultimate/boogie/ast/IfThenExpression.java rename trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/{VerificationExpression.java => StateRecoverabilityVerificationCondition.java} (53%) rename trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/{VerificationExpressionContainer.java => StateRecoverabilityVerificationConditionContainer.java} (82%) diff --git a/trunk/source/Library-BoogieAST/src/de/uni_freiburg/informatik/ultimate/boogie/ExpressionFactory.java b/trunk/source/Library-BoogieAST/src/de/uni_freiburg/informatik/ultimate/boogie/ExpressionFactory.java index 2e7f917b061..ed78d01a8b6 100644 --- a/trunk/source/Library-BoogieAST/src/de/uni_freiburg/informatik/ultimate/boogie/ExpressionFactory.java +++ b/trunk/source/Library-BoogieAST/src/de/uni_freiburg/informatik/ultimate/boogie/ExpressionFactory.java @@ -49,6 +49,7 @@ import de.uni_freiburg.informatik.ultimate.boogie.ast.FunctionApplication; import de.uni_freiburg.informatik.ultimate.boogie.ast.IdentifierExpression; import de.uni_freiburg.informatik.ultimate.boogie.ast.IfThenElseExpression; +import de.uni_freiburg.informatik.ultimate.boogie.ast.IfThenExpression; import de.uni_freiburg.informatik.ultimate.boogie.ast.IntegerLiteral; import de.uni_freiburg.informatik.ultimate.boogie.ast.LeftHandSide; import de.uni_freiburg.informatik.ultimate.boogie.ast.RealLiteral; @@ -397,7 +398,7 @@ private static Expression constructBinExprWithLiteralOpsBitvector(final ILocatio throw new AssertionError("unknown operator " + operator); } } - + public static Expression constructIfThenExpression(final ILocation loc, final Expression condition, final Expression thenPart) { if (condition instanceof BooleanLiteral) { @@ -406,12 +407,12 @@ public static Expression constructIfThenExpression(final ILocation loc, final Ex return thenPart; } } - final BoogieType type = TypeCheckHelper.typeCheckIfThenElseExpression((BoogieType) condition.getType(), + final BoogieType type = TypeCheckHelper.typeCheckIfThenExpression((BoogieType) condition.getType(), (BoogieType) thenPart.getType(), (BoogieType) thenPart.getType(), new TypeErrorReporter(loc)); - return new IfThenElseExpression(loc, type, condition, thenPart, null); + return new IfThenExpression(loc, type, condition, thenPart); } - + public static Expression constructIfThenElseExpression(final ILocation loc, final Expression condition, final Expression thenPart, final Expression elsePart) { if (condition instanceof BooleanLiteral) { diff --git a/trunk/source/Library-BoogieAST/src/de/uni_freiburg/informatik/ultimate/boogie/ast/IfThenExpression.java b/trunk/source/Library-BoogieAST/src/de/uni_freiburg/informatik/ultimate/boogie/ast/IfThenExpression.java new file mode 100644 index 00000000000..bb700446673 --- /dev/null +++ b/trunk/source/Library-BoogieAST/src/de/uni_freiburg/informatik/ultimate/boogie/ast/IfThenExpression.java @@ -0,0 +1,120 @@ +package de.uni_freiburg.informatik.ultimate.boogie.ast; + +import java.util.List; + +import de.uni_freiburg.informatik.ultimate.core.model.models.IBoogieType; +import de.uni_freiburg.informatik.ultimate.core.model.models.ILocation; + +public class IfThenExpression extends Expression{ + + private static final long serialVersionUID = 1L; + private static final java.util.function.Predicate VALIDATOR = + BoogieASTNode.VALIDATORS.get(IfThenElseExpression.class); + /** + * The condition of this if then expression. + */ + Expression condition; + + /** + * The then part of this if then expression. + */ + Expression thenPart; + + /** + * The constructor taking initial values. + * @param loc the location of this node + * @param condition the condition of this if then else expression. + * @param thenPart the then part of this if then else expression. + */ + public IfThenExpression(ILocation loc, Expression condition, Expression thenPart) { + super(loc); + this.condition = condition; + this.thenPart = thenPart; + assert VALIDATOR == null || VALIDATOR.test(this) : "Invalid IfThenExpression: " + this; + } + + /** + * The constructor taking initial values. + * @param loc the location of this node + * @param type the type of this expression. + * @param condition the condition of this if then else expression. + * @param thenPart the then part of this if then else expression. + */ + public IfThenExpression(ILocation loc, IBoogieType type, Expression condition, Expression thenPart) { + super(loc, type); + this.condition = condition; + this.thenPart = thenPart; + assert VALIDATOR == null || VALIDATOR.test(this) : "Invalid IfThenExpression: " + this; + } + + /** + * Returns a textual description of this object. + */ + public String toString() { + StringBuffer sb = new StringBuffer(); + sb.append("IfThenElseExpression").append('['); + sb.append(condition); + sb.append(',').append(thenPart); + return sb.append(']').toString(); + } + + /** + * Gets the condition of this if then else expression. + * @return the condition of this if then else expression. + */ + public Expression getCondition() { + return condition; + } + + /** + * Gets the then part of this if then else expression. + * @return the then part of this if then else expression. + */ + public Expression getThenPart() { + return thenPart; + } + + public List getOutgoingNodes() { + List children = super.getOutgoingNodes(); + children.add(condition); + children.add(thenPart); + return children; + } + + public void accept(GeneratedBoogieAstVisitor visitor) { + if (visitor.visit((Expression)this)) { + //visit parent types higher up if necessary + } else { + return; + } + if (visitor.visit(this)) { + if(condition!=null){ + condition.accept(visitor); + } + if(thenPart!=null){ + thenPart.accept(visitor); + } + } + } + + public Expression accept(GeneratedBoogieAstTransformer visitor) { + Expression node = visitor.transform(this); + if(node != this){ + return node; + } + + Expression newcondition = null; + if(condition != null){ + newcondition = (Expression)condition.accept(visitor); + } + Expression newthenPart = null; + if(thenPart != null){ + newthenPart = (Expression)thenPart.accept(visitor); + } + if(condition != newcondition || thenPart != newthenPart){ + return new IfThenExpression(loc, type, newcondition, newthenPart); + } + return this; + } + +} diff --git a/trunk/source/Library-BoogieAST/src/de/uni_freiburg/informatik/ultimate/boogie/typechecker/TypeCheckHelper.java b/trunk/source/Library-BoogieAST/src/de/uni_freiburg/informatik/ultimate/boogie/typechecker/TypeCheckHelper.java index 30f88fb63af..3ce178ee0d2 100644 --- a/trunk/source/Library-BoogieAST/src/de/uni_freiburg/informatik/ultimate/boogie/typechecker/TypeCheckHelper.java +++ b/trunk/source/Library-BoogieAST/src/de/uni_freiburg/informatik/ultimate/boogie/typechecker/TypeCheckHelper.java @@ -265,6 +265,23 @@ public static BoogieType typeCheckIfThenElseExpression(final BoogieType cond } return resultType; } + + public static BoogieType typeCheckIfThenExpression(final BoogieType condType, final BoogieType left, + final BoogieType right, final ITypeErrorReporter typeErrorReporter) { + BoogieType resultType; + if (!condType.equals(BoogieType.TYPE_ERROR) && !condType.equals(BoogieType.TYPE_BOOL)) { + // typeError(expr, "if expects boolean type: " + expr); + typeErrorReporter.report(exp -> "if expects boolean type: " + exp); + } + if (!left.isUnifiableTo(right)) { + // typeError(expr, "Type check failed for " + expr); + typeErrorReporter.report(exp -> "Type check failed for " + exp); + resultType = BoogieType.TYPE_ERROR; + } else { + resultType = left.equals(BoogieType.TYPE_ERROR) ? right : left; + } + return resultType; + } public static void typeCheckAssignStatement(final String[] lhsIds, final BoogieType[] lhsTypes, final BoogieType[] rhsTypes, final ITypeErrorReporter typeErrorReporter) { diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/PEAtoBoogieObserver.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/PEAtoBoogieObserver.java index cbb46891a70..9cd78cd665f 100644 --- a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/PEAtoBoogieObserver.java +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/PEAtoBoogieObserver.java @@ -56,6 +56,7 @@ private IElement generateBoogie(final List> patterns) { if (mode == PEATransformerMode.REQ_CHECK) { return generateReqCheckBoogie(patterns); } + // For checks with additional parameters that must be passed for execution. if (mode == PEATransformerMode.REQ_PARAM_CHECK) { return generateReqParamCheckBoogie(patterns); } @@ -76,6 +77,7 @@ private IElement generateReqCheckBoogie(final List> patterns) { return translator.getUnit(); } + // For checks with additional parameters that must be passed for execution. private IElement generateReqParamCheckBoogie(final List> patterns) { final Req2ModifySymbolTablePeaTransformer transformer = new Req2ModifySymbolTablePeaTransformer(mServices, mLogger); diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/req2pea/ReqCheckAnnotator.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/req2pea/ReqCheckAnnotator.java index 41e62b5320e..8a9dfafd88e 100644 --- a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/req2pea/ReqCheckAnnotator.java +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/req2pea/ReqCheckAnnotator.java @@ -81,7 +81,7 @@ import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.PeaPhaseProgramCounter; import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.StateRecoverabilityAuxiliaryStatement; import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.StateRecoverabilityGenerator; -import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.VerificationExpression; +import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.StateRecoverabilityVerificationCondition; import de.uni_freiburg.informatik.ultimate.pea2boogie.translator.CheckedReqLocation; import de.uni_freiburg.informatik.ultimate.util.CoreUtil; import de.uni_freiburg.informatik.ultimate.util.datastructures.CrossProducts; @@ -198,10 +198,10 @@ private List genCheckStateRecoverability(final BoogieLocation bl) { List statements = new ArrayList<>(); StateRecoverabilityGenerator stateRecoverabilityGenerator = new StateRecoverabilityGenerator(); AuxiliaryStatementContainer auxStatementContainer = mSymbolTable.getAuxStatementContainer(); - Map>> vePeaAuxStatementMap = stateRecoverabilityGenerator.getAuxStatementPerVerificationExpression(auxStatementContainer); + Map>> vePeaAuxStatementMap = stateRecoverabilityGenerator.getAuxStatementPerVerificationExpression(auxStatementContainer); - for(Map.Entry>> entry : vePeaAuxStatementMap.entrySet()) { - VerificationExpression ve = entry.getKey(); + for(Map.Entry>> entry : vePeaAuxStatementMap.entrySet()) { + StateRecoverabilityVerificationCondition ve = entry.getKey(); for(Map.Entry> entryPeaStRecAuxSt : entry.getValue().entrySet()) { Set stRecAuxStSet = entryPeaStRecAuxSt.getValue(); diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/StateRecoverabilityAuxiliaryStatement.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/StateRecoverabilityAuxiliaryStatement.java index f21fc98926d..ac2e74b015f 100644 --- a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/StateRecoverabilityAuxiliaryStatement.java +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/StateRecoverabilityAuxiliaryStatement.java @@ -46,7 +46,7 @@ public class StateRecoverabilityAuxiliaryStatement implements AuxiliaryStatement private BoogieLocation loc; private String pcVariable; private int pc; - private VerificationExpression verificationExpression; + private StateRecoverabilityVerificationCondition verificationExpression; private Statement declVar; private Statement assignVar; private Statement ifSt; @@ -55,7 +55,7 @@ public StateRecoverabilityAuxiliaryStatement(String variable) { this.relatedVariable = variable; } - public StateRecoverabilityAuxiliaryStatement(PeaPhaseProgramCounter peaPhasePc, String variable, String pcVariable, int pc, VerificationExpression ve) { + public StateRecoverabilityAuxiliaryStatement(PeaPhaseProgramCounter peaPhasePc, String variable, String pcVariable, int pc, StateRecoverabilityVerificationCondition ve) { this.peaPhasePc = peaPhasePc; this.relatedVariable = variable; this.pcVariable = pcVariable; @@ -103,11 +103,11 @@ public void setPc(int pc) { this.pc = pc; } - public VerificationExpression getVerificationExpression() { + public StateRecoverabilityVerificationCondition getVerificationExpression() { return verificationExpression; } - public void setVerificationExpression(VerificationExpression verificationExpression) { + public void setVerificationExpression(StateRecoverabilityVerificationCondition verificationExpression) { this.verificationExpression = verificationExpression; } diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/StateRecoverabilityGenerator.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/StateRecoverabilityGenerator.java index c582b1068eb..3fd55e49725 100644 --- a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/StateRecoverabilityGenerator.java +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/StateRecoverabilityGenerator.java @@ -131,9 +131,9 @@ public StateRecoverabilityGenerator(final ILogger logger, final IUltimateService mCddToSmt = new CddToSmt(mServices, mPeaResultUtil, mScript, mBoogie2Smt, boogieDeclarations, mReqSymboltable); } - public Map> - getRelevantLocationsFromPea(List reqPeasList, VerificationExpressionContainer vec) { - Map> veLocation = new HashMap<>(); + public Map> + getRelevantLocationsFromPea(List reqPeasList, StateRecoverabilityVerificationConditionContainer vec) { + Map> veLocation = new HashMap<>(); Set reqPeasSet = new HashSet<>(reqPeasList); Set declaredConstants = new HashSet<>(); Map reqPeasTerm = new HashMap<>(); @@ -155,7 +155,7 @@ public StateRecoverabilityGenerator(final ILogger logger, final IUltimateService // Check for every phase if the location can fulfill the verification expression // TRUE -> Do not add the phase // FALSE -> Add the phase - for (VerificationExpression ve : vec.getVerificationExpressions().values()) { + for (StateRecoverabilityVerificationCondition ve : vec.getVerificationExpressions().values()) { CDD veCcd = BoogieBooleanExpressionDecision .create(createOppositeCondition(new DefaultLocation(), ve.getBoogiePrimitiveType(), ve.getVariable(), ve.getOperator(), ve.getValue())); @@ -312,9 +312,9 @@ private static Script buildSolver(final IUltimateServiceProvider services) throw return SolverBuilder.buildAndInitializeSolver(services, settings, "RtInconsistencySolver"); } - public Map>> + public Map>> getAuxStatementPerVerificationExpression(AuxiliaryStatementContainer auxStatementContainer) { - Map>> vePeaAuxStatementMap = + Map>> vePeaAuxStatementMap = new HashMap<>(); for (AuxiliaryStatement auxStatement : auxStatementContainer.getSreMap().values()) { if (auxStatement instanceof StateRecoverabilityAuxiliaryStatement) { diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/VerificationExpression.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/StateRecoverabilityVerificationCondition.java similarity index 53% rename from trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/VerificationExpression.java rename to trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/StateRecoverabilityVerificationCondition.java index 413da3a414c..53908c8233b 100644 --- a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/VerificationExpression.java +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/StateRecoverabilityVerificationCondition.java @@ -31,68 +31,75 @@ import de.uni_freiburg.informatik.ultimate.boogie.type.BoogiePrimitiveType; /** -* -* @author Tobias Wießner -* -*/ + * + * This class contains a condition to be verified for the property check state-recoverability. An object of this class + * is created via each condition entered in the GUI. + * + * @author Tobias Wießner + * + */ -public class VerificationExpression { +public class StateRecoverabilityVerificationCondition { private final String[] expr; private final String dataType; private final int iVariable = 0; private final int iOperator = 1; private final int iValue = 2; - public VerificationExpression(String[] expr, String dataType) { - this.expr = expr; - this.dataType = dataType; - } - public String[] getExpr() { - return expr; - } - - public String getVariable() { - return expr[iVariable]; - } - - public String getOperator() { - return expr[iOperator]; - } - - public String getValue() { - return expr[iValue]; - } - - public String getDataType( ) { - return dataType; - } - - public boolean getBoolValue() { - if(expr[iValue].equals(VerificationExpressionContainer.BOOL)) { - return Boolean.getBoolean(expr[iValue]); - } - - throw new RuntimeErrorException(null, getClass().getName() + " data type " + dataType + " is not correct for " + expr); - } - - public int getIntegerValue() { - if(expr[iValue].equals(VerificationExpressionContainer.INT)) { - return Integer.getInteger(expr[iValue]); - } - - throw new RuntimeErrorException(null, getClass().getName() + " data type " + dataType + " is not correct for " + expr); - } - - public double getDoubleValue() { - if(expr[iValue].equals(VerificationExpressionContainer.REAL)) { - return Double.parseDouble(expr[iValue]); - } - - throw new RuntimeErrorException(null, getClass().getName() + " data type " + dataType + " is not correct for " + expr); - } - - public BoogiePrimitiveType getBoogiePrimitiveType() { - switch (dataType) { + public StateRecoverabilityVerificationCondition(String[] expr, String dataType) { + this.expr = expr; + this.dataType = dataType; + } + + public String[] getExpr() { + return expr; + } + + public String getVariable() { + return expr[iVariable]; + } + + public String getOperator() { + return expr[iOperator]; + } + + public String getValue() { + return expr[iValue]; + } + + public String getDataType() { + return dataType; + } + + public boolean getBoolValue() { + if (expr[iValue].equals(StateRecoverabilityVerificationConditionContainer.BOOL)) { + return Boolean.getBoolean(expr[iValue]); + } + + throw new RuntimeErrorException(null, + getClass().getName() + " data type " + dataType + " is not correct for " + expr); + } + + public int getIntegerValue() { + if (expr[iValue].equals(StateRecoverabilityVerificationConditionContainer.INT)) { + return Integer.getInteger(expr[iValue]); + } + + throw new RuntimeErrorException(null, + getClass().getName() + " data type " + dataType + " is not correct for " + expr); + } + + public double getDoubleValue() { + if (expr[iValue].equals(StateRecoverabilityVerificationConditionContainer.REAL)) { + return Double.parseDouble(expr[iValue]); + } + + throw new RuntimeErrorException(null, + getClass().getName() + " data type " + dataType + " is not correct for " + expr); + } + + public BoogiePrimitiveType getBoogiePrimitiveType() { + switch (dataType) { case "bool": return BoogiePrimitiveType.TYPE_BOOL; case "int": @@ -102,5 +109,5 @@ public BoogiePrimitiveType getBoogiePrimitiveType() { default: return BoogiePrimitiveType.TYPE_ERROR; } - } + } } diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/VerificationExpressionContainer.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/StateRecoverabilityVerificationConditionContainer.java similarity index 82% rename from trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/VerificationExpressionContainer.java rename to trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/StateRecoverabilityVerificationConditionContainer.java index c9ca397277d..21907b05907 100644 --- a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/VerificationExpressionContainer.java +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/StateRecoverabilityVerificationConditionContainer.java @@ -43,11 +43,13 @@ /** * +* This class contains all conditions to be verified for the property check state-recoverability. +* * @author Tobias Wießner * */ -public class VerificationExpressionContainer { +public class StateRecoverabilityVerificationConditionContainer { // Pattern for input expression public static final String exprPattern = "\\s{0,1}((\\w+)\\s*([<>=!][=]*)\\s*(\\w+))\\s{0,1}"; @@ -58,10 +60,10 @@ public class VerificationExpressionContainer { public static final String REAL = "real"; private IReq2Pea mReq2pea; - private Map mVerificationExpressions; + private Map mVerificationExpressions; private Map mVariableDataTypeMap; - public VerificationExpressionContainer(IReq2Pea req2pea) { + public StateRecoverabilityVerificationConditionContainer(IReq2Pea req2pea) { mReq2pea = req2pea; mVerificationExpressions = new HashMap<>(); getDataTypeFromReq2Pea(req2pea); @@ -82,12 +84,12 @@ private void getDataTypeFromReq2Pea(IReq2Pea req2Pea) { mVariableDataTypeMap = variableDataTypeMap; } - public Map getVerificationExpressions() { + public Map getVerificationExpressions() { return mVerificationExpressions; } public void addExpression(String inputExpr) { - List veList = new ArrayList<>(); + List veList = new ArrayList<>(); int grpVariable = 2; int grpOperator = 3; int grpValue = 4; @@ -103,19 +105,19 @@ public void addExpression(String inputExpr) { throw new IllegalArgumentException( getClass().getName() + " could not find data type for " + sVariable); } - veList.add(new VerificationExpression(new String[] { sVariable, sOperator, sValue }, dataType)); + veList.add(new StateRecoverabilityVerificationCondition(new String[] { sVariable, sOperator, sValue }, dataType)); } } addVerificationExpression(veList); } - private void addVerificationExpression(List veList) { - for (VerificationExpression ve : veList) { + private void addVerificationExpression(List veList) { + for (StateRecoverabilityVerificationCondition ve : veList) { addVerificationExpression(ve); } } - private void addVerificationExpression(VerificationExpression ve) { + private void addVerificationExpression(StateRecoverabilityVerificationCondition ve) { if (mVerificationExpressions == null) { mVerificationExpressions = new HashMap<>(); } diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/testgen/Req2ModifySymbolTablePea.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/testgen/Req2ModifySymbolTablePea.java index 83f95b38cc1..35fe00d4482 100644 --- a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/testgen/Req2ModifySymbolTablePea.java +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/testgen/Req2ModifySymbolTablePea.java @@ -49,8 +49,8 @@ import de.uni_freiburg.informatik.ultimate.pea2boogie.req2pea.IReq2Pea; import de.uni_freiburg.informatik.ultimate.pea2boogie.req2pea.IReq2PeaAnnotator; import de.uni_freiburg.informatik.ultimate.pea2boogie.req2pea.ReqCheckAnnotator; -import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.VerificationExpression; -import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.VerificationExpressionContainer; +import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.StateRecoverabilityVerificationCondition; +import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.StateRecoverabilityVerificationConditionContainer; import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.AuxiliaryStatement; import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.PeaPhaseProgramCounter; import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.StateRecoverabilityAuxiliaryStatement; @@ -98,7 +98,7 @@ public Durations getDurations() { @Override public void transform(IReq2Pea req2pea) { - final VerificationExpressionContainer vec = getVerificationExpression(req2pea); + final StateRecoverabilityVerificationConditionContainer vec = getVerificationExpression(req2pea); final List simplePeas = req2pea.getReqPeas(); final IReqSymbolTable oldSymbolTable = req2pea.getSymboltable(); @@ -123,7 +123,7 @@ public void transform(IReq2Pea req2pea) { //Collecting the PEAs and ProgramCounter //Necessary in Transformer since otherwise unused global variables would be in the Boogie code - Map> veLocationMap = stRecGen.getRelevantLocationsFromPea(simplePeas, vec); + Map> veLocationMap = stRecGen.getRelevantLocationsFromPea(simplePeas, vec); List sreList = createGlobalVariableForVerificationExpression(builder, veLocationMap, vec); @@ -138,7 +138,7 @@ private void createIfStatementInWhileLoop(List auxStatements for(AuxiliaryStatement auxStatement : auxStatements) { if(auxStatement instanceof StateRecoverabilityAuxiliaryStatement) { StateRecoverabilityAuxiliaryStatement auxStatementStRec = (StateRecoverabilityAuxiliaryStatement) auxStatement; - VerificationExpression ve = auxStatementStRec.getVerificationExpression(); + StateRecoverabilityVerificationCondition ve = auxStatementStRec.getVerificationExpression(); ILocation loc = auxStatementStRec.getBoogieLocation(); // Create expression //Opposite of verification Expression @@ -155,17 +155,17 @@ private void createIfStatementInWhileLoop(List auxStatements } } - private VerificationExpressionContainer getVerificationExpression(IReq2Pea req2pea) { - final VerificationExpressionContainer vec = new VerificationExpressionContainer(req2pea); + private StateRecoverabilityVerificationConditionContainer getVerificationExpression(IReq2Pea req2pea) { + final StateRecoverabilityVerificationConditionContainer vec = new StateRecoverabilityVerificationConditionContainer(req2pea); //Gets verification expression from GUI String verExpr = prefs.getString(Pea2BoogiePreferences.LABEL_STATE_RECOVERABILITY_VER_EXPR); vec.addExpression(verExpr); return vec; } - private List createGlobalVariableForVerificationExpression(ReqSymboltableBuilder builder, Map> veLocationMaptionMap, VerificationExpressionContainer vec) { + private List createGlobalVariableForVerificationExpression(ReqSymboltableBuilder builder, Map> veLocationMaptionMap, StateRecoverabilityVerificationConditionContainer vec) { List sreList = new ArrayList<>(); - for(Map.Entry> entry : veLocationMaptionMap.entrySet()) { + for(Map.Entry> entry : veLocationMaptionMap.entrySet()) { for(PeaPhaseProgramCounter peaPhasePc : entry.getValue()) { String pcName = getPcName(peaPhasePc.getPea().getName()); int pc = peaPhasePc.getPc(); From 503cb86ab90469a8f2052c35aad225e065dfa768 Mon Sep 17 00:00:00 2001 From: Tobias Wiessner Date: Tue, 29 Aug 2023 17:18:38 +0200 Subject: [PATCH 16/23] Bugfix --- .../informatik/ultimate/boogie/ast/IfThenExpression.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/trunk/source/Library-BoogieAST/src/de/uni_freiburg/informatik/ultimate/boogie/ast/IfThenExpression.java b/trunk/source/Library-BoogieAST/src/de/uni_freiburg/informatik/ultimate/boogie/ast/IfThenExpression.java index bb700446673..1b7d6094ee5 100644 --- a/trunk/source/Library-BoogieAST/src/de/uni_freiburg/informatik/ultimate/boogie/ast/IfThenExpression.java +++ b/trunk/source/Library-BoogieAST/src/de/uni_freiburg/informatik/ultimate/boogie/ast/IfThenExpression.java @@ -9,7 +9,7 @@ public class IfThenExpression extends Expression{ private static final long serialVersionUID = 1L; private static final java.util.function.Predicate VALIDATOR = - BoogieASTNode.VALIDATORS.get(IfThenElseExpression.class); + BoogieASTNode.VALIDATORS.get(IfThenExpression.class); /** * The condition of this if then expression. */ From bb7fa8e8e96bc8f25557fc69437235accc441a26 Mon Sep 17 00:00:00 2001 From: Tobias Wiessner Date: Wed, 30 Aug 2023 07:12:22 +0200 Subject: [PATCH 17/23] Bugfix --- .../ultimate/boogie/ExpressionFactory.java | 14 -- .../ultimate/boogie/ast/IfThenExpression.java | 120 ------------------ .../ReqCheckStateRecoverabilityResult.java | 2 +- .../testgen/Req2ModifySymbolTablePea.java | 13 -- 4 files changed, 1 insertion(+), 148 deletions(-) delete mode 100644 trunk/source/Library-BoogieAST/src/de/uni_freiburg/informatik/ultimate/boogie/ast/IfThenExpression.java diff --git a/trunk/source/Library-BoogieAST/src/de/uni_freiburg/informatik/ultimate/boogie/ExpressionFactory.java b/trunk/source/Library-BoogieAST/src/de/uni_freiburg/informatik/ultimate/boogie/ExpressionFactory.java index ed78d01a8b6..40f969c7a17 100644 --- a/trunk/source/Library-BoogieAST/src/de/uni_freiburg/informatik/ultimate/boogie/ExpressionFactory.java +++ b/trunk/source/Library-BoogieAST/src/de/uni_freiburg/informatik/ultimate/boogie/ExpressionFactory.java @@ -399,20 +399,6 @@ private static Expression constructBinExprWithLiteralOpsBitvector(final ILocatio } } - public static Expression constructIfThenExpression(final ILocation loc, final Expression condition, - final Expression thenPart) { - if (condition instanceof BooleanLiteral) { - final boolean value = ((BooleanLiteral) condition).getValue(); - if (value) { - return thenPart; - } - } - final BoogieType type = TypeCheckHelper.typeCheckIfThenExpression((BoogieType) condition.getType(), - (BoogieType) thenPart.getType(), (BoogieType) thenPart.getType(), new TypeErrorReporter(loc)); - return new IfThenExpression(loc, type, condition, thenPart); - - } - public static Expression constructIfThenElseExpression(final ILocation loc, final Expression condition, final Expression thenPart, final Expression elsePart) { if (condition instanceof BooleanLiteral) { diff --git a/trunk/source/Library-BoogieAST/src/de/uni_freiburg/informatik/ultimate/boogie/ast/IfThenExpression.java b/trunk/source/Library-BoogieAST/src/de/uni_freiburg/informatik/ultimate/boogie/ast/IfThenExpression.java deleted file mode 100644 index 1b7d6094ee5..00000000000 --- a/trunk/source/Library-BoogieAST/src/de/uni_freiburg/informatik/ultimate/boogie/ast/IfThenExpression.java +++ /dev/null @@ -1,120 +0,0 @@ -package de.uni_freiburg.informatik.ultimate.boogie.ast; - -import java.util.List; - -import de.uni_freiburg.informatik.ultimate.core.model.models.IBoogieType; -import de.uni_freiburg.informatik.ultimate.core.model.models.ILocation; - -public class IfThenExpression extends Expression{ - - private static final long serialVersionUID = 1L; - private static final java.util.function.Predicate VALIDATOR = - BoogieASTNode.VALIDATORS.get(IfThenExpression.class); - /** - * The condition of this if then expression. - */ - Expression condition; - - /** - * The then part of this if then expression. - */ - Expression thenPart; - - /** - * The constructor taking initial values. - * @param loc the location of this node - * @param condition the condition of this if then else expression. - * @param thenPart the then part of this if then else expression. - */ - public IfThenExpression(ILocation loc, Expression condition, Expression thenPart) { - super(loc); - this.condition = condition; - this.thenPart = thenPart; - assert VALIDATOR == null || VALIDATOR.test(this) : "Invalid IfThenExpression: " + this; - } - - /** - * The constructor taking initial values. - * @param loc the location of this node - * @param type the type of this expression. - * @param condition the condition of this if then else expression. - * @param thenPart the then part of this if then else expression. - */ - public IfThenExpression(ILocation loc, IBoogieType type, Expression condition, Expression thenPart) { - super(loc, type); - this.condition = condition; - this.thenPart = thenPart; - assert VALIDATOR == null || VALIDATOR.test(this) : "Invalid IfThenExpression: " + this; - } - - /** - * Returns a textual description of this object. - */ - public String toString() { - StringBuffer sb = new StringBuffer(); - sb.append("IfThenElseExpression").append('['); - sb.append(condition); - sb.append(',').append(thenPart); - return sb.append(']').toString(); - } - - /** - * Gets the condition of this if then else expression. - * @return the condition of this if then else expression. - */ - public Expression getCondition() { - return condition; - } - - /** - * Gets the then part of this if then else expression. - * @return the then part of this if then else expression. - */ - public Expression getThenPart() { - return thenPart; - } - - public List getOutgoingNodes() { - List children = super.getOutgoingNodes(); - children.add(condition); - children.add(thenPart); - return children; - } - - public void accept(GeneratedBoogieAstVisitor visitor) { - if (visitor.visit((Expression)this)) { - //visit parent types higher up if necessary - } else { - return; - } - if (visitor.visit(this)) { - if(condition!=null){ - condition.accept(visitor); - } - if(thenPart!=null){ - thenPart.accept(visitor); - } - } - } - - public Expression accept(GeneratedBoogieAstTransformer visitor) { - Expression node = visitor.transform(this); - if(node != this){ - return node; - } - - Expression newcondition = null; - if(condition != null){ - newcondition = (Expression)condition.accept(visitor); - } - Expression newthenPart = null; - if(thenPart != null){ - newthenPart = (Expression)thenPart.accept(visitor); - } - if(condition != newcondition || thenPart != newthenPart){ - return new IfThenExpression(loc, type, newcondition, newthenPart); - } - return this; - } - -} diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/results/ReqCheckStateRecoverabilityResult.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/results/ReqCheckStateRecoverabilityResult.java index 9615f953903..c6d2682a617 100644 --- a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/results/ReqCheckStateRecoverabilityResult.java +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/results/ReqCheckStateRecoverabilityResult.java @@ -52,7 +52,7 @@ public String getLongDescription() { sb.append(getShortDescription()); sb.append(CoreUtil.getPlatformLineSeparator()); if (mMessage != null) { - sb.append("Verification Expression: "); + sb.append("Verification Condition: "); sb.append(mMessage); } return sb.toString(); diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/testgen/Req2ModifySymbolTablePea.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/testgen/Req2ModifySymbolTablePea.java index 35fe00d4482..2b9d55d6361 100644 --- a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/testgen/Req2ModifySymbolTablePea.java +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/testgen/Req2ModifySymbolTablePea.java @@ -219,19 +219,6 @@ private static AssignmentStatement genAssignmentStmt(final ILocation bl, final V private ILocation constructNewLocation() { return new DefaultLocation(); } - - private IBoogieType getBoogieType(String type) { - switch (type.toLowerCase()) { - case "bool": - case "real": - case "int": - return BoogiePrimitiveType.toPrimitiveType(type); - case "event": - return BoogieType.TYPE_BOOL; - default: - return BoogieType.TYPE_ERROR; - } - } @Override public boolean hasErrors() { From d6637baa79f47259c32c5a445938e527f2d3adc2 Mon Sep 17 00:00:00 2001 From: Tobias Wiessner Date: Wed, 30 Aug 2023 07:18:47 +0200 Subject: [PATCH 18/23] Removed import --- .../informatik/ultimate/boogie/ExpressionFactory.java | 1 - 1 file changed, 1 deletion(-) diff --git a/trunk/source/Library-BoogieAST/src/de/uni_freiburg/informatik/ultimate/boogie/ExpressionFactory.java b/trunk/source/Library-BoogieAST/src/de/uni_freiburg/informatik/ultimate/boogie/ExpressionFactory.java index 40f969c7a17..75bc83a0da3 100644 --- a/trunk/source/Library-BoogieAST/src/de/uni_freiburg/informatik/ultimate/boogie/ExpressionFactory.java +++ b/trunk/source/Library-BoogieAST/src/de/uni_freiburg/informatik/ultimate/boogie/ExpressionFactory.java @@ -49,7 +49,6 @@ import de.uni_freiburg.informatik.ultimate.boogie.ast.FunctionApplication; import de.uni_freiburg.informatik.ultimate.boogie.ast.IdentifierExpression; import de.uni_freiburg.informatik.ultimate.boogie.ast.IfThenElseExpression; -import de.uni_freiburg.informatik.ultimate.boogie.ast.IfThenExpression; import de.uni_freiburg.informatik.ultimate.boogie.ast.IntegerLiteral; import de.uni_freiburg.informatik.ultimate.boogie.ast.LeftHandSide; import de.uni_freiburg.informatik.ultimate.boogie.ast.RealLiteral; From 6c6b86ae339a3e634946c1c519ce6a9fabc95b1d Mon Sep 17 00:00:00 2001 From: Tobias Wiessner Date: Thu, 31 Aug 2023 11:02:50 +0200 Subject: [PATCH 19/23] Verification Condition as Expression --- .../pea2boogie/req2pea/ReqCheckAnnotator.java | 2 +- .../StateRecoverabilityGenerator.java | 31 ++++++++++--------- ...teRecoverabilityVerificationCondition.java | 20 ++++++++---- ...abilityVerificationConditionContainer.java | 8 ++--- 4 files changed, 35 insertions(+), 26 deletions(-) diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/req2pea/ReqCheckAnnotator.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/req2pea/ReqCheckAnnotator.java index 8a9dfafd88e..89c781eaa78 100644 --- a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/req2pea/ReqCheckAnnotator.java +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/req2pea/ReqCheckAnnotator.java @@ -213,7 +213,7 @@ private List genCheckStateRecoverability(final BoogieLocation bl) { Expression andCondition = ExpressionFactory.newBinaryExpression(bl, Operator.LOGICAND, globalVariableTrue, inputCondition); Expression expr = ExpressionFactory.constructUnaryExpression(bl, UnaryExpression.Operator.LOGICNEG, andCondition); - final ReqCheck check = createReqCheck(Spec.STATE_RECOVERABILITY, stRecAuxSt.getPeaPhasePc().getReq(), entryPeaStRecAuxSt.getKey(), String.join("", ve.getExpr())); + final ReqCheck check = createReqCheck(Spec.STATE_RECOVERABILITY, stRecAuxSt.getPeaPhasePc().getReq(), entryPeaStRecAuxSt.getKey(), String.join("", ve.getVerificationConditionStrings())); statements .add(createAssert(expr, check, checkLabel)); } } diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/StateRecoverabilityGenerator.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/StateRecoverabilityGenerator.java index 3fd55e49725..0cd4f46361d 100644 --- a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/StateRecoverabilityGenerator.java +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/StateRecoverabilityGenerator.java @@ -89,10 +89,10 @@ import de.uni_freiburg.informatik.ultimate.util.ConstructionCache; /** -* -* @author Tobias Wießner -* -*/ + * + * @author Tobias Wießner + * + */ public class StateRecoverabilityGenerator { @@ -131,8 +131,8 @@ public StateRecoverabilityGenerator(final ILogger logger, final IUltimateService mCddToSmt = new CddToSmt(mServices, mPeaResultUtil, mScript, mBoogie2Smt, boogieDeclarations, mReqSymboltable); } - public Map> - getRelevantLocationsFromPea(List reqPeasList, StateRecoverabilityVerificationConditionContainer vec) { + public Map> getRelevantLocationsFromPea( + List reqPeasList, StateRecoverabilityVerificationConditionContainer vec) { Map> veLocation = new HashMap<>(); Set reqPeasSet = new HashSet<>(reqPeasList); Set declaredConstants = new HashSet<>(); @@ -156,13 +156,14 @@ public StateRecoverabilityGenerator(final ILogger logger, final IUltimateService // TRUE -> Do not add the phase // FALSE -> Add the phase for (StateRecoverabilityVerificationCondition ve : vec.getVerificationExpressions().values()) { - CDD veCcd = BoogieBooleanExpressionDecision - .create(createOppositeCondition(new DefaultLocation(), ve.getBoogiePrimitiveType(), - ve.getVariable(), ve.getOperator(), ve.getValue())); + CDD verificationConditionCcd = BoogieBooleanExpressionDecision.create(ExpressionFactory.constructUnaryExpression( + ve.getVerificationConditionExpression().getLoc(), + de.uni_freiburg.informatik.ultimate.boogie.ast.UnaryExpression.Operator.LOGICNEG, + ve.getVerificationConditionExpression())); List invariantVeList = new ArrayList<>(); // Compute phase invariant ⋀ opposite verification expression - final Term termVe = mCddToSmt.toSmt(veCcd); + final Term termVe = mCddToSmt.toSmt(verificationConditionCcd); invariantVeList.add(termVe); final Term termLocation = mCddToSmt.toSmt(phase.getStateInvariant()); invariantVeList.add(termLocation); @@ -386,7 +387,7 @@ public Expression createExpression(final ILocation loc, BoogieType boogieType, S return expression; } - public Expression createExpression(final ILocation loc, BoogieType boogieType, String sLhs, String sOpr, + public static Expression createExpression(final ILocation loc, BoogieType boogieType, String sLhs, String sOpr, String sRhs) { Expression rhs = null; Expression lhs; @@ -404,14 +405,15 @@ public Expression createExpression(final ILocation loc, BoogieType boogieType, S rhs = ExpressionFactory.createRealLiteral(loc, sRhs); break; case "type-error": - throw new RuntimeErrorException(null, getClass().getName() + ": " + boogieType + " no known data type."); + throw new RuntimeErrorException(null, + StateRecoverabilityGenerator.class.getName() + ": " + boogieType + " no known data type."); } opr = getOperator(sOpr); Expression expression = ExpressionFactory.newBinaryExpression(loc, opr, lhs, rhs); return expression; } - private BinaryExpression.Operator getOperator(String sOpr) { + private static BinaryExpression.Operator getOperator(String sOpr) { switch (sOpr) { case "||": case "|": @@ -432,7 +434,8 @@ private BinaryExpression.Operator getOperator(String sOpr) { case ">=": return Operator.COMPGEQ; default: - throw new RuntimeErrorException(null, getClass().getName() + ": Could not parse operator."); + throw new RuntimeErrorException(null, + StateRecoverabilityGenerator.class.getName() + ": Could not parse operator."); } } } diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/StateRecoverabilityVerificationCondition.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/StateRecoverabilityVerificationCondition.java index 53908c8233b..7bf6b2b38e3 100644 --- a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/StateRecoverabilityVerificationCondition.java +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/StateRecoverabilityVerificationCondition.java @@ -28,7 +28,9 @@ import javax.management.RuntimeErrorException; +import de.uni_freiburg.informatik.ultimate.boogie.ast.Expression; import de.uni_freiburg.informatik.ultimate.boogie.type.BoogiePrimitiveType; +import de.uni_freiburg.informatik.ultimate.core.lib.models.annotation.DefaultLocation; /** * @@ -40,6 +42,7 @@ */ public class StateRecoverabilityVerificationCondition { + private final Expression verificationConditionExpression; private final String[] expr; private final String dataType; private final int iVariable = 0; @@ -49,9 +52,14 @@ public class StateRecoverabilityVerificationCondition { public StateRecoverabilityVerificationCondition(String[] expr, String dataType) { this.expr = expr; this.dataType = dataType; + this.verificationConditionExpression = StateRecoverabilityGenerator.createExpression(new DefaultLocation(), getBoogiePrimitiveType(dataType), expr[iVariable], expr[iOperator], expr[iValue]); + } + + public Expression getVerificationConditionExpression() { + return verificationConditionExpression; } - public String[] getExpr() { + public String[] getVerificationConditionStrings() { return expr; } @@ -72,7 +80,7 @@ public String getDataType() { } public boolean getBoolValue() { - if (expr[iValue].equals(StateRecoverabilityVerificationConditionContainer.BOOL)) { + if (BoogiePrimitiveType.TYPE_BOOL.equals(getBoogiePrimitiveType(dataType))) { return Boolean.getBoolean(expr[iValue]); } @@ -81,7 +89,7 @@ public boolean getBoolValue() { } public int getIntegerValue() { - if (expr[iValue].equals(StateRecoverabilityVerificationConditionContainer.INT)) { + if (BoogiePrimitiveType.TYPE_INT.equals(getBoogiePrimitiveType(dataType))) { return Integer.getInteger(expr[iValue]); } @@ -90,7 +98,7 @@ public int getIntegerValue() { } public double getDoubleValue() { - if (expr[iValue].equals(StateRecoverabilityVerificationConditionContainer.REAL)) { + if (BoogiePrimitiveType.TYPE_REAL.equals(getBoogiePrimitiveType(dataType))) { return Double.parseDouble(expr[iValue]); } @@ -98,8 +106,8 @@ public double getDoubleValue() { getClass().getName() + " data type " + dataType + " is not correct for " + expr); } - public BoogiePrimitiveType getBoogiePrimitiveType() { - switch (dataType) { + public BoogiePrimitiveType getBoogiePrimitiveType(String sDataType) { + switch (sDataType) { case "bool": return BoogiePrimitiveType.TYPE_BOOL; case "int": diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/StateRecoverabilityVerificationConditionContainer.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/StateRecoverabilityVerificationConditionContainer.java index 21907b05907..8f8237b3834 100644 --- a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/StateRecoverabilityVerificationConditionContainer.java +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/StateRecoverabilityVerificationConditionContainer.java @@ -36,6 +36,9 @@ import javax.management.RuntimeErrorException; +import de.uni_freiburg.informatik.ultimate.boogie.ast.Expression; +import de.uni_freiburg.informatik.ultimate.boogie.type.BoogiePrimitiveType; +import de.uni_freiburg.informatik.ultimate.core.lib.models.annotation.DefaultLocation; import de.uni_freiburg.informatik.ultimate.lib.pea.CounterTrace; import de.uni_freiburg.informatik.ultimate.lib.pea.PhaseEventAutomata; import de.uni_freiburg.informatik.ultimate.lib.srparse.pattern.PatternType.ReqPeas; @@ -54,11 +57,6 @@ public class StateRecoverabilityVerificationConditionContainer { // Pattern for input expression public static final String exprPattern = "\\s{0,1}((\\w+)\\s*([<>=!][=]*)\\s*(\\w+))\\s{0,1}"; - // Data types - public static final String BOOL = "bool"; - public static final String INT = "int"; - public static final String REAL = "real"; - private IReq2Pea mReq2pea; private Map mVerificationExpressions; private Map mVariableDataTypeMap; From a76734039262cfa1e116042aaddc59c7a18e8f9a Mon Sep 17 00:00:00 2001 From: Tobias Wiessner Date: Thu, 31 Aug 2023 11:06:39 +0200 Subject: [PATCH 20/23] Review fix --- .../ultimate/pea2boogie/req2pea/ReqCheckAnnotator.java | 2 +- .../StateRecoverabilityVerificationCondition.java | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/req2pea/ReqCheckAnnotator.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/req2pea/ReqCheckAnnotator.java index 89c781eaa78..5c12ce40161 100644 --- a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/req2pea/ReqCheckAnnotator.java +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/req2pea/ReqCheckAnnotator.java @@ -213,7 +213,7 @@ private List genCheckStateRecoverability(final BoogieLocation bl) { Expression andCondition = ExpressionFactory.newBinaryExpression(bl, Operator.LOGICAND, globalVariableTrue, inputCondition); Expression expr = ExpressionFactory.constructUnaryExpression(bl, UnaryExpression.Operator.LOGICNEG, andCondition); - final ReqCheck check = createReqCheck(Spec.STATE_RECOVERABILITY, stRecAuxSt.getPeaPhasePc().getReq(), entryPeaStRecAuxSt.getKey(), String.join("", ve.getVerificationConditionStrings())); + final ReqCheck check = createReqCheck(Spec.STATE_RECOVERABILITY, stRecAuxSt.getPeaPhasePc().getReq(), entryPeaStRecAuxSt.getKey(), String.join("", ve.getVerificationConditionString())); statements .add(createAssert(expr, check, checkLabel)); } } diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/StateRecoverabilityVerificationCondition.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/StateRecoverabilityVerificationCondition.java index 7bf6b2b38e3..b3d5be06ae3 100644 --- a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/StateRecoverabilityVerificationCondition.java +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/StateRecoverabilityVerificationCondition.java @@ -59,7 +59,7 @@ public Expression getVerificationConditionExpression() { return verificationConditionExpression; } - public String[] getVerificationConditionStrings() { + public String[] getVerificationConditionString() { return expr; } From b55702b5966666212c631db0bf7e0840ced2389a Mon Sep 17 00:00:00 2001 From: Tobias Wiessner Date: Sun, 3 Sep 2023 16:24:11 +0200 Subject: [PATCH 21/23] Bugfix for property check without any assertations --- .../staterecoverability/StateRecoverabilityGenerator.java | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/StateRecoverabilityGenerator.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/StateRecoverabilityGenerator.java index 0cd4f46361d..7ed4fd9204c 100644 --- a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/StateRecoverabilityGenerator.java +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/StateRecoverabilityGenerator.java @@ -280,7 +280,13 @@ private Term generateParallelAutomatonTerm(Set reqPeas) { reqsCDD.and(peasCDD); } } - final Term term = mCddToSmt.toSmt(reqsCDD); + // Check for Null in case there is no start location, then deliver a false condition + Term term; + if(reqsCDD != null) { + term = mCddToSmt.toSmt(reqsCDD); + } else { + term = mCddToSmt.toSmt(CDD.FALSE); + } return term; } From f09372a6c75b96e1a6931975e617d05a65c8071a Mon Sep 17 00:00:00 2001 From: Tobias Wiessner Date: Sat, 23 Sep 2023 12:42:48 +0200 Subject: [PATCH 22/23] Bugfix --- .../pea2boogie/req2pea/ReqCheckAnnotator.java | 3 +- .../StateRecoverabilityGenerator.java | 38 ++++++++++++++----- 2 files changed, 30 insertions(+), 11 deletions(-) diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/req2pea/ReqCheckAnnotator.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/req2pea/ReqCheckAnnotator.java index 5c12ce40161..43e1efc0f24 100644 --- a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/req2pea/ReqCheckAnnotator.java +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/req2pea/ReqCheckAnnotator.java @@ -214,8 +214,7 @@ private List genCheckStateRecoverability(final BoogieLocation bl) { Expression expr = ExpressionFactory.constructUnaryExpression(bl, UnaryExpression.Operator.LOGICNEG, andCondition); final ReqCheck check = createReqCheck(Spec.STATE_RECOVERABILITY, stRecAuxSt.getPeaPhasePc().getReq(), entryPeaStRecAuxSt.getKey(), String.join("", ve.getVerificationConditionString())); - statements .add(createAssert(expr, check, checkLabel)); - } + statements .add(createAssert(expr, check, checkLabel)); } } } diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/StateRecoverabilityGenerator.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/StateRecoverabilityGenerator.java index 7ed4fd9204c..f48d5f2272a 100644 --- a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/StateRecoverabilityGenerator.java +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/StateRecoverabilityGenerator.java @@ -136,13 +136,26 @@ public Map Map> veLocation = new HashMap<>(); Set reqPeasSet = new HashSet<>(reqPeasList); Set declaredConstants = new HashSet<>(); - Map reqPeasTerm = new HashMap<>(); + Map> termPerPhase = new HashMap<>(); - // Create Terms for every location + // Create Terms for every location for (ReqPeas reqPeas : reqPeasList) { List> ctPeaList = reqPeas.getCounterTrace2Pea(); - Term parallelAutomaton = generateParallelAutomatonTerm(removeReqPeas(reqPeasSet, reqPeas)); - reqPeasTerm.put(reqPeas, parallelAutomaton); + + for(Entry entry : ctPeaList) { + PhaseEventAutomata pea = entry.getValue(); + Phase[] phases = pea.getPhases(); + for (int i = 0; i < phases.length; ++i) { + Phase phase = phases[i]; + CDD invariantPhaseGuardCDD = phase.getStateInvariant().and(phase.getClockInvariant()); + Term parallelAutomaton = generateParallelAutomatonTerm(removeReqPeas(reqPeasSet, reqPeas), invariantPhaseGuardCDD); + + if(!termPerPhase.containsKey(reqPeas)) { + termPerPhase.put(reqPeas, new HashMap<>()); + } + termPerPhase.get(reqPeas).put(phase, parallelAutomaton); + } + } } for (ReqPeas reqPea : reqPeasList) { @@ -176,9 +189,10 @@ public Map veLocation.put(ve, new HashSet<>()); } + //Term possibleStartPhase = + //possibleStartPhase(phase, reqPea, reqPeasTerm.get(reqPea), termVe); Term possibleStartPhase = - possibleStartPhase(phase, reqPea, reqPeasTerm.get(reqPea), termVe); - + possibleStartPhase(phase, reqPea, termPerPhase.get(reqPea).get(phase), termVe); // Declare constants for Z3 declareConstants(mScript, possibleStartPhase, declaredConstants); @@ -237,8 +251,8 @@ private Set removeReqPeas(Set reqPeasSet, ReqPeas reqPeas) { * * @param reqPeas * @return term - */ - private Term generateParallelAutomatonTerm(Set reqPeas) { + */ + private Term generateParallelAutomatonTerm(Set reqPeas, CDD currentReqLocationCDD) { Map reqPeasPeaArrayMap = createPeaArray(reqPeas); CDD reqsCDD = null; for (Map.Entry entry : reqPeasPeaArrayMap.entrySet()) { @@ -257,7 +271,7 @@ private Term generateParallelAutomatonTerm(Set reqPeas) { invariantPhaseGuardArrayPerPea[i] = invariantPhaseGuardCDD; } - // Link every location-guard CDD with OR + // Link every location invariant-guard CDD with OR CDD peaCDD = null; for (int i = 0; i < invariantPhaseGuardArrayPerPea.length; ++i) { if (peaCDD == null) { @@ -280,6 +294,12 @@ private Term generateParallelAutomatonTerm(Set reqPeas) { reqsCDD.and(peasCDD); } } + // Attaches the current req location CDD to the CDDs of all other requirements + if(reqsCDD != null) { + reqsCDD.and(currentReqLocationCDD); + } else { + reqsCDD = currentReqLocationCDD; + } // Check for Null in case there is no start location, then deliver a false condition Term term; if(reqsCDD != null) { From 7d75049d0506c319eefeefc0823d95ed1eee721d Mon Sep 17 00:00:00 2001 From: Tobias Wiessner Date: Tue, 21 Nov 2023 11:57:33 +0100 Subject: [PATCH 23/23] Resolve Boogie data type issue --- .../ultimate/pea2boogie/req2pea/ReqCheckAnnotator.java | 2 +- ...teRecoverabilityVerificationConditionContainer.java | 10 ++++++++-- .../pea2boogie/testgen/Req2ModifySymbolTablePea.java | 5 +++-- .../pea2boogie/translator/ReqSymboltableBuilder.java | 5 +++++ .../ultimate/reqtotest/req/Req2TestReqSymbolTable.java | 6 ++++++ 5 files changed, 23 insertions(+), 5 deletions(-) diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/req2pea/ReqCheckAnnotator.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/req2pea/ReqCheckAnnotator.java index 43e1efc0f24..97ff8b464b0 100644 --- a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/req2pea/ReqCheckAnnotator.java +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/req2pea/ReqCheckAnnotator.java @@ -96,7 +96,7 @@ public class ReqCheckAnnotator implements IReq2PeaAnnotator { private static final boolean DEBUG_ONLY_FIRST_NON_TRIVIAL_RT_INCONSISTENCY = false; - private static final boolean PRINT_PEA_DOT = true; + private static final boolean PRINT_PEA_DOT = false; private final ILogger mLogger; private final IUltimateServiceProvider mServices; diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/StateRecoverabilityVerificationConditionContainer.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/StateRecoverabilityVerificationConditionContainer.java index 8f8237b3834..054cf854207 100644 --- a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/StateRecoverabilityVerificationConditionContainer.java +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/StateRecoverabilityVerificationConditionContainer.java @@ -38,6 +38,7 @@ import de.uni_freiburg.informatik.ultimate.boogie.ast.Expression; import de.uni_freiburg.informatik.ultimate.boogie.type.BoogiePrimitiveType; +import de.uni_freiburg.informatik.ultimate.boogie.type.BoogieType; import de.uni_freiburg.informatik.ultimate.core.lib.models.annotation.DefaultLocation; import de.uni_freiburg.informatik.ultimate.lib.pea.CounterTrace; import de.uni_freiburg.informatik.ultimate.lib.pea.PhaseEventAutomata; @@ -100,8 +101,13 @@ public void addExpression(String inputExpr) { String sValue = m.group(grpValue); String dataType = mVariableDataTypeMap.get(sVariable); if (dataType == null) { - throw new IllegalArgumentException( - getClass().getName() + " could not find data type for " + sVariable); + BoogieType boogieType = mReq2pea.getSymboltable().getId2Type().get(sVariable); + dataType = boogieType.toString(); + if(dataType == null) { + throw new IllegalArgumentException( + getClass().getName() + " could not find data type for " + sVariable); + } + } veList.add(new StateRecoverabilityVerificationCondition(new String[] { sVariable, sOperator, sValue }, dataType)); } diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/testgen/Req2ModifySymbolTablePea.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/testgen/Req2ModifySymbolTablePea.java index 2b9d55d6361..e42989f6bef 100644 --- a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/testgen/Req2ModifySymbolTablePea.java +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/testgen/Req2ModifySymbolTablePea.java @@ -98,10 +98,11 @@ public Durations getDurations() { @Override public void transform(IReq2Pea req2pea) { - final StateRecoverabilityVerificationConditionContainer vec = getVerificationExpression(req2pea); - final List simplePeas = req2pea.getReqPeas(); final IReqSymbolTable oldSymbolTable = req2pea.getSymboltable(); + + final StateRecoverabilityVerificationConditionContainer vec = getVerificationExpression(req2pea); + stRecGen = new StateRecoverabilityGenerator(mLogger, mServices, oldSymbolTable); final ReqSymboltableBuilder builder = new ReqSymboltableBuilder(mLogger, oldSymbolTable); diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/translator/ReqSymboltableBuilder.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/translator/ReqSymboltableBuilder.java index 18c2ddc70ac..f130348bc99 100644 --- a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/translator/ReqSymboltableBuilder.java +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/translator/ReqSymboltableBuilder.java @@ -555,6 +555,11 @@ public String getPrimedVarId(final String name) { public String getHistoryVarId(final String name) { return ReqSymboltableBuilder.getHistoryVarId(name); } + + @Override + public Map getId2Type() { + return mId2Type; + } @Override public Collection getDeclarations() { diff --git a/trunk/source/ReqToTest/src/de/uni_freiburg/informatik/ultimate/reqtotest/req/Req2TestReqSymbolTable.java b/trunk/source/ReqToTest/src/de/uni_freiburg/informatik/ultimate/reqtotest/req/Req2TestReqSymbolTable.java index edc100b98bd..f22aaae3403 100644 --- a/trunk/source/ReqToTest/src/de/uni_freiburg/informatik/ultimate/reqtotest/req/Req2TestReqSymbolTable.java +++ b/trunk/source/ReqToTest/src/de/uni_freiburg/informatik/ultimate/reqtotest/req/Req2TestReqSymbolTable.java @@ -376,4 +376,10 @@ public AuxiliaryStatementContainer getAuxStatementContainer() { return null; } + @Override + public Map getId2Type() { + // TODO Auto-generated method stub + return null; + } + }