Add support for new property check for requirements called State-Recoverability

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) {

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:

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<T> {
 		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<String> {
+
+			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 <Variable<Operator>VALUE, ...>";
+			}
+		}
+
+		default Matcher match(String s, String pattern) {
+			Pattern p = Pattern.compile(pattern);
+	        Matcher m = p.matcher(s);
+	        return m;
+		}
 	}
 
 }

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

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<String> getClockVars();
 
 	Set<String> getStateVars();
+
+	Set<String> getAuxVars();
+
+	AuxStatementContainer getAuxStatementContainer();
 
 	/**
 	 * Given a variable name, return the name of the primed version of this variable.

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,22 +56,36 @@ private IElement generateBoogie(final List<PatternType<?>> 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);
 		}
 		return null;
 	}
 
 	private IElement generateReqCheckBoogie(final List<PatternType<?>> 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.
 		final UnaryOperator<IResult> resultTransformer = reporter::convertTraceAbstractionResult;
 		mServices.getResultService().registerTransformer("CexReducer", resultTransformer);
 		return translator.getUnit();
 	}
+
+	private IElement generateReqParamCheckBoogie(final List<PatternType<?>> 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<IResult> resultTransformer = reporter::convertTraceAbstractionResult;
+		mServices.getResultService().registerTransformer("CexReducer", resultTransformer);
+		return translator.getUnit();
+	}
 
 	private IElement generateReqTestBoogie(final List<PatternType<?>> patterns) {
 		// TODO: would it be nicer to get the symbol table via annotations?

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);

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];

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,