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

trunk/source/Library-BoogieAST/src/de/uni_freiburg/informatik/ultimate/boogie/typechecker/TypeCheckHelper.java

@@ -265,6 +265,23 @@ public static <T> BoogieType typeCheckIfThenElseExpression(final BoogieType cond
 		}
 		return resultType;
 	}
+
+	public static <T> BoogieType typeCheckIfThenExpression(final BoogieType condType, final BoogieType left,
+			final BoogieType right, final ITypeErrorReporter<T> 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 <T> void typeCheckAssignStatement(final String[] lhsIds, final BoogieType[] lhsTypes,
 			final BoogieType[] rhsTypes, final ITypeErrorReporter<T> typeErrorReporter) {

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.AuxiliaryStatementContainer;
 import de.uni_freiburg.informatik.ultimate.util.datastructures.UnionFind;
 
 public interface IReqSymbolTable {
@@ -66,6 +68,12 @@ public interface IReqSymbolTable {
 
 	Set<String> getStateVars();
 
+	// Allows you to easily add more elements to the Boogie program at any line without the need to create more
+	// interface methods.
+	Set<String> getAuxVars();
+
+	AuxiliaryStatementContainer 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,6 +56,10 @@ private IElement generateBoogie(final List<PatternType<?>> 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);
+		}
 		if (mode == PEATransformerMode.REQ_TEST) {
 			return generateReqTestBoogie(patterns);
 		}
@@ -72,6 +77,22 @@ private IElement generateReqCheckBoogie(final List<PatternType<?>> patterns) {
 		return translator.getUnit();
 	}
 
+	// For checks with additional parameters that must be passed for execution.
+	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?
 		final Req2CauseTrackingPeaTransformer transformer = new Req2CauseTrackingPeaTransformer(mServices, mLogger);

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,13 @@ 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 +565,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/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;
@@ -81,6 +80,18 @@ 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 = 
+			"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";
+
 	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 +110,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() {
@@ -110,28 +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_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) {