From 5886ba9fffef83ff1f8c453def2f76d4abe02101 Mon Sep 17 00:00:00 2001 From: Dennis Hendriks <dh_tue@hotmail.com> Date: Fri, 26 Jul 2024 14:05:41 +0200 Subject: [PATCH 01/16] #424 ExplorerPreChecker: comment out existing code. --- .../cif/explorer/ExplorerPreChecker.java | 472 ++++++++---------- 1 file changed, 221 insertions(+), 251 deletions(-) diff --git a/cif/org.eclipse.escet.cif.explorer/src/org/eclipse/escet/cif/explorer/ExplorerPreChecker.java b/cif/org.eclipse.escet.cif.explorer/src/org/eclipse/escet/cif/explorer/ExplorerPreChecker.java index 6f4a0b74fb..886e899202 100644 --- a/cif/org.eclipse.escet.cif.explorer/src/org/eclipse/escet/cif/explorer/ExplorerPreChecker.java +++ b/cif/org.eclipse.escet.cif.explorer/src/org/eclipse/escet/cif/explorer/ExplorerPreChecker.java @@ -13,259 +13,229 @@ package org.eclipse.escet.cif.explorer; -import static org.eclipse.escet.common.java.Sets.set; -import static org.eclipse.escet.common.java.Sets.sortedstrings; -import static org.eclipse.escet.common.java.Strings.fmt; - -import java.util.EnumSet; -import java.util.List; -import java.util.Set; - -import org.eclipse.emf.ecore.EObject; -import org.eclipse.escet.cif.common.CifMath; -import org.eclipse.escet.cif.common.CifTextUtils; -import org.eclipse.escet.cif.common.CifTypeUtils; -import org.eclipse.escet.cif.common.CifValueUtils; -import org.eclipse.escet.cif.metamodel.cif.ComplexComponent; -import org.eclipse.escet.cif.metamodel.cif.Invariant; -import org.eclipse.escet.cif.metamodel.cif.Specification; -import org.eclipse.escet.cif.metamodel.cif.automata.Automaton; -import org.eclipse.escet.cif.metamodel.cif.automata.Edge; -import org.eclipse.escet.cif.metamodel.cif.automata.EdgeEvent; -import org.eclipse.escet.cif.metamodel.cif.automata.Location; -import org.eclipse.escet.cif.metamodel.cif.declarations.DiscVariable; -import org.eclipse.escet.cif.metamodel.cif.declarations.InputVariable; -import org.eclipse.escet.cif.metamodel.cif.expressions.ContVariableExpression; -import org.eclipse.escet.cif.metamodel.cif.expressions.Expression; -import org.eclipse.escet.cif.metamodel.cif.expressions.StdLibFunctionExpression; -import org.eclipse.escet.cif.metamodel.cif.expressions.TauExpression; -import org.eclipse.escet.cif.metamodel.cif.functions.ExternalFunction; -import org.eclipse.escet.cif.metamodel.cif.types.DistType; import org.eclipse.escet.cif.metamodel.java.CifWalker; -import org.eclipse.escet.common.java.Assert; -import org.eclipse.escet.common.java.exceptions.UnsupportedException; /** Checker class to verify that a given specification satisfies the pre-conditions required for exploration. */ public class ExplorerPreChecker extends CifWalker { - /** Found problems in the specification. */ - private Set<String> problems = null; - - /** Set of configurable properties to check. */ - private final EnumSet<CheckParameters> params; - - /** - * Constructor of the {@link ExplorerPreChecker} class. - * - * @param params Set of configurable parameters for the explorer pre-checker. - */ - public ExplorerPreChecker(EnumSet<CheckParameters> params) { - this.params = params; - } - - /** - * Check the specification for the requirements. - * - * @param spec Specification to check. - */ - public void checkSpec(Specification spec) { - problems = set(); - walkSpecification(spec); - - if (problems.isEmpty()) { - return; - } - - // If we have any problems, the specification is unsupported. - String msg = "State space exploration failed due to unsatisfied preconditions:\n - " - + String.join("\n - ", sortedstrings(problems)); - throw new UnsupportedException(msg); - } - - /** Parameters of the explorer check process. */ - public static enum CheckParameters { - /** Allow 'none' invariants. */ - ALLOW_NON_INVS, - - /** Allow 'supervisor' invariants. */ - ALLOW_SUP_INVS, - - /** Allow 'requirement' invariants. */ - ALLOW_REQ_INVS, - - /** Allow 'none' automaton. */ - ALLOW_NON_AUT, - - /** Allow 'supervisor' automaton. */ - ALLOW_SUP_AUT, - - /** Allow 'requirement' automaton. */ - ALLOW_REQ_AUT, - - /** Allow 'tau' events. */ - ALLOW_TAU, - } - - @Override - protected void preprocessDistType(DistType tp) { - String msg = fmt("Distribution type \"%s\" is not supported.", CifTextUtils.typeToStr(tp)); - problems.add(msg); - } - - @Override - protected void preprocessAutomaton(Automaton aut) { - String msg; - - switch (aut.getKind()) { - case NONE: - if (params.contains(CheckParameters.ALLOW_NON_AUT)) { - break; - } - msg = fmt("Regular automaton \"%s\" is not supported.", CifTextUtils.getAbsName(aut)); - problems.add(msg); - break; - - case PLANT: - break; // Always supported. - - case REQUIREMENT: - if (params.contains(CheckParameters.ALLOW_REQ_AUT)) { - break; - } - msg = fmt("Requirement automaton \"%s\" is not supported.", CifTextUtils.getAbsName(aut)); - problems.add(msg); - break; - - case SUPERVISOR: - if (params.contains(CheckParameters.ALLOW_SUP_AUT)) { - break; - } - msg = fmt("Supervisor automaton \"%s\" is not supported.", CifTextUtils.getAbsName(aut)); - problems.add(msg); - break; - } - } - - @Override - protected void preprocessEdge(Edge edge) { - if (params.contains(CheckParameters.ALLOW_TAU)) { - return; - } - - String msg; - Location loc = (Location)edge.eContainer(); - if (edge.getEvents().isEmpty()) { - msg = fmt("Tau events in edges of %s are not supported.", CifTextUtils.getLocationText2(loc)); - problems.add(msg); - return; - } - for (EdgeEvent ee: edge.getEvents()) { - if (ee.getEvent() instanceof TauExpression) { - msg = fmt("Tau events in edges of %s are not supported.", CifTextUtils.getLocationText2(loc)); - problems.add(msg); - return; - } - } - } - - @Override - protected void preprocessExternalFunction(ExternalFunction func) { - String msg = fmt("External user-defined function \"%s\" is not supported.", CifTextUtils.getAbsName(func)); - problems.add(msg); - } - - @Override - protected void preprocessInputVariable(InputVariable var) { - String msg = fmt("Input variable \"%s\" is not supported.", CifTextUtils.getAbsName(var)); - problems.add(msg); - } - - @Override - protected void preprocessDiscVariable(DiscVariable var) { - // Single initial value is always OK. - if (var.getValue() == null) { - return; - } - List<Expression> initVals = var.getValue().getValues(); - if (initVals.size() == 1) { - return; - } - - // Finite number of potential initial values is always OK. - if (!initVals.isEmpty()) { - return; - } - - // Any value in its domain. Check for finite type. That is, the number - // of possible values must fit within the range of 'int', to ensure we - // can store the potential values in a list. - double cnt = CifValueUtils.getPossibleValueCount(var.getType()); - if (cnt <= Integer.MAX_VALUE) { - return; - } - - // Unsupported type for multiple initial values. - String cntTxt = Double.isInfinite(cnt) ? "infinite" : CifMath.realToStr(cnt); - String msg = fmt("Discrete variable \"%s\" of type \"%s\" with %s potential initial values is not supported.", - CifTextUtils.getAbsName(var), CifTextUtils.typeToStr(var.getType()), cntTxt); - problems.add(msg); - } - - @Override - protected void preprocessInvariant(Invariant inv) { - EObject parent = inv.eContainer(); - String parentTxt; - if (parent instanceof Location) { - parentTxt = CifTextUtils.getLocationText2((Location)parent); - } else { - Assert.check(parent instanceof ComplexComponent); - parentTxt = CifTextUtils.getComponentText2((ComplexComponent)parent); - } - - String msg; - switch (inv.getSupKind()) { - case NONE: - if (params.contains(CheckParameters.ALLOW_NON_INVS)) { - break; - } - msg = fmt("Regular invariants in %s are not supported.", parentTxt); - problems.add(msg); - break; - - case PLANT: - break; // Always supported. - - case REQUIREMENT: - if (params.contains(CheckParameters.ALLOW_REQ_INVS)) { - break; - } - msg = fmt("Requirement invariants in %s are not supported.", parentTxt); - problems.add(msg); - break; - - case SUPERVISOR: - if (params.contains(CheckParameters.ALLOW_SUP_INVS)) { - break; - } - msg = fmt("Supervisor invariants in %s are not supported.", parentTxt); - problems.add(msg); - break; - } - } - - @Override - protected void preprocessContVariableExpression(ContVariableExpression expr) { - if (expr.isDerivative()) { - String msg = "Use of derivatives of continuous variables is not supported."; - problems.add(msg); - } - } - - @Override - protected void preprocessStdLibFunctionExpression(StdLibFunctionExpression expr) { - if (CifTypeUtils.isDistFunction(expr.getFunction())) { - String msg = fmt("Distribution standard library function \"%s\" is not supported.", - CifTextUtils.functionToStr(expr.getFunction())); - problems.add(msg); - } - } +// /** Found problems in the specification. */ +// private Set<String> problems = null; +// +// /** Set of configurable properties to check. */ +// private final EnumSet<CheckParameters> params; +// +// /** +// * Constructor of the {@link ExplorerPreChecker} class. +// * +// * @param params Set of configurable parameters for the explorer pre-checker. +// */ +// public ExplorerPreChecker(EnumSet<CheckParameters> params) { +// this.params = params; +// } +// +// /** +// * Check the specification for the requirements. +// * +// * @param spec Specification to check. +// */ +// public void checkSpec(Specification spec) { +// problems = set(); +// walkSpecification(spec); +// +// if (problems.isEmpty()) { +// return; +// } +// +// // If we have any problems, the specification is unsupported. +// String msg = "State space exploration failed due to unsatisfied preconditions:\n - " +// + String.join("\n - ", sortedstrings(problems)); +// throw new UnsupportedException(msg); +// } +// +// /** Parameters of the explorer check process. */ +// public static enum CheckParameters { +// /** Allow 'none' invariants. */ +// ALLOW_NON_INVS, +// +// /** Allow 'supervisor' invariants. */ +// ALLOW_SUP_INVS, +// +// /** Allow 'requirement' invariants. */ +// ALLOW_REQ_INVS, +// +// /** Allow 'none' automaton. */ +// ALLOW_NON_AUT, +// +// /** Allow 'supervisor' automaton. */ +// ALLOW_SUP_AUT, +// +// /** Allow 'requirement' automaton. */ +// ALLOW_REQ_AUT, +// +// /** Allow 'tau' events. */ +// ALLOW_TAU, +// } +// +// @Override +// protected void preprocessDistType(DistType tp) { +// String msg = fmt("Distribution type \"%s\" is not supported.", CifTextUtils.typeToStr(tp)); +// problems.add(msg); +// } +// +// @Override +// protected void preprocessAutomaton(Automaton aut) { +// String msg; +// +// switch (aut.getKind()) { +// case NONE: +// if (params.contains(CheckParameters.ALLOW_NON_AUT)) { +// break; +// } +// msg = fmt("Regular automaton \"%s\" is not supported.", CifTextUtils.getAbsName(aut)); +// problems.add(msg); +// break; +// +// case PLANT: +// break; // Always supported. +// +// case REQUIREMENT: +// if (params.contains(CheckParameters.ALLOW_REQ_AUT)) { +// break; +// } +// msg = fmt("Requirement automaton \"%s\" is not supported.", CifTextUtils.getAbsName(aut)); +// problems.add(msg); +// break; +// +// case SUPERVISOR: +// if (params.contains(CheckParameters.ALLOW_SUP_AUT)) { +// break; +// } +// msg = fmt("Supervisor automaton \"%s\" is not supported.", CifTextUtils.getAbsName(aut)); +// problems.add(msg); +// break; +// } +// } +// +// @Override +// protected void preprocessEdge(Edge edge) { +// if (params.contains(CheckParameters.ALLOW_TAU)) { +// return; +// } +// +// String msg; +// Location loc = (Location)edge.eContainer(); +// if (edge.getEvents().isEmpty()) { +// msg = fmt("Tau events in edges of %s are not supported.", CifTextUtils.getLocationText2(loc)); +// problems.add(msg); +// return; +// } +// for (EdgeEvent ee: edge.getEvents()) { +// if (ee.getEvent() instanceof TauExpression) { +// msg = fmt("Tau events in edges of %s are not supported.", CifTextUtils.getLocationText2(loc)); +// problems.add(msg); +// return; +// } +// } +// } +// +// @Override +// protected void preprocessExternalFunction(ExternalFunction func) { +// String msg = fmt("External user-defined function \"%s\" is not supported.", CifTextUtils.getAbsName(func)); +// problems.add(msg); +// } +// +// @Override +// protected void preprocessInputVariable(InputVariable var) { +// String msg = fmt("Input variable \"%s\" is not supported.", CifTextUtils.getAbsName(var)); +// problems.add(msg); +// } +// +// @Override +// protected void preprocessDiscVariable(DiscVariable var) { +// // Single initial value is always OK. +// if (var.getValue() == null) { +// return; +// } +// List<Expression> initVals = var.getValue().getValues(); +// if (initVals.size() == 1) { +// return; +// } +// +// // Finite number of potential initial values is always OK. +// if (!initVals.isEmpty()) { +// return; +// } +// +// // Any value in its domain. Check for finite type. That is, the number +// // of possible values must fit within the range of 'int', to ensure we +// // can store the potential values in a list. +// double cnt = CifValueUtils.getPossibleValueCount(var.getType()); +// if (cnt <= Integer.MAX_VALUE) { +// return; +// } +// +// // Unsupported type for multiple initial values. +// String cntTxt = Double.isInfinite(cnt) ? "infinite" : CifMath.realToStr(cnt); +// String msg = fmt("Discrete variable \"%s\" of type \"%s\" with %s potential initial values is not supported.", +// CifTextUtils.getAbsName(var), CifTextUtils.typeToStr(var.getType()), cntTxt); +// problems.add(msg); +// } +// +// @Override +// protected void preprocessInvariant(Invariant inv) { +// EObject parent = inv.eContainer(); +// String parentTxt; +// if (parent instanceof Location) { +// parentTxt = CifTextUtils.getLocationText2((Location)parent); +// } else { +// Assert.check(parent instanceof ComplexComponent); +// parentTxt = CifTextUtils.getComponentText2((ComplexComponent)parent); +// } +// +// String msg; +// switch (inv.getSupKind()) { +// case NONE: +// if (params.contains(CheckParameters.ALLOW_NON_INVS)) { +// break; +// } +// msg = fmt("Regular invariants in %s are not supported.", parentTxt); +// problems.add(msg); +// break; +// +// case PLANT: +// break; // Always supported. +// +// case REQUIREMENT: +// if (params.contains(CheckParameters.ALLOW_REQ_INVS)) { +// break; +// } +// msg = fmt("Requirement invariants in %s are not supported.", parentTxt); +// problems.add(msg); +// break; +// +// case SUPERVISOR: +// if (params.contains(CheckParameters.ALLOW_SUP_INVS)) { +// break; +// } +// msg = fmt("Supervisor invariants in %s are not supported.", parentTxt); +// problems.add(msg); +// break; +// } +// } +// +// @Override +// protected void preprocessContVariableExpression(ContVariableExpression expr) { +// if (expr.isDerivative()) { +// String msg = "Use of derivatives of continuous variables is not supported."; +// problems.add(msg); +// } +// } +// +// @Override +// protected void preprocessStdLibFunctionExpression(StdLibFunctionExpression expr) { +// if (CifTypeUtils.isDistFunction(expr.getFunction())) { +// String msg = fmt("Distribution standard library function \"%s\" is not supported.", +// CifTextUtils.functionToStr(expr.getFunction())); +// problems.add(msg); +// } +// } } -- GitLab From 002f2b40343b4ea4950d29bb04a9b84774fc4ac8 Mon Sep 17 00:00:00 2001 From: Dennis Hendriks <dh_tue@hotmail.com> Date: Fri, 26 Jul 2024 14:07:29 +0200 Subject: [PATCH 02/16] #424 ExplorerPreChecker: prepare empty checker using new framework. --- .../escet/cif/explorer/ExplorerPreChecker.java | 18 +++++++++++++++--- 1 file changed, 15 insertions(+), 3 deletions(-) diff --git a/cif/org.eclipse.escet.cif.explorer/src/org/eclipse/escet/cif/explorer/ExplorerPreChecker.java b/cif/org.eclipse.escet.cif.explorer/src/org/eclipse/escet/cif/explorer/ExplorerPreChecker.java index 886e899202..9236dabe36 100644 --- a/cif/org.eclipse.escet.cif.explorer/src/org/eclipse/escet/cif/explorer/ExplorerPreChecker.java +++ b/cif/org.eclipse.escet.cif.explorer/src/org/eclipse/escet/cif/explorer/ExplorerPreChecker.java @@ -13,10 +13,22 @@ package org.eclipse.escet.cif.explorer; -import org.eclipse.escet.cif.metamodel.java.CifWalker; +import org.eclipse.escet.cif.checkers.CifPreconditionChecker; +import org.eclipse.escet.common.java.Termination; + +/** CIF explorer precondition checker. */ +public class ExplorerPreChecker extends CifPreconditionChecker { + /** + * Constructor for the {@link ExplorerPreChecker} class. + * + * @param termination Cooperative termination query function. + */ + public ExplorerPreChecker(Termination termination) { + super(termination + + ); + } -/** Checker class to verify that a given specification satisfies the pre-conditions required for exploration. */ -public class ExplorerPreChecker extends CifWalker { // /** Found problems in the specification. */ // private Set<String> problems = null; // -- GitLab From 8d4f982b1c90b6530682743345052c849168b066 Mon Sep 17 00:00:00 2001 From: Dennis Hendriks <dh_tue@hotmail.com> Date: Fri, 26 Jul 2024 14:13:11 +0200 Subject: [PATCH 03/16] #424 ExplorerPreChecker: move 'no distributions' check. --- .../cif/explorer/ExplorerPreChecker.java | 25 +++++++------------ 1 file changed, 9 insertions(+), 16 deletions(-) diff --git a/cif/org.eclipse.escet.cif.explorer/src/org/eclipse/escet/cif/explorer/ExplorerPreChecker.java b/cif/org.eclipse.escet.cif.explorer/src/org/eclipse/escet/cif/explorer/ExplorerPreChecker.java index 9236dabe36..7c0cdb2bbd 100644 --- a/cif/org.eclipse.escet.cif.explorer/src/org/eclipse/escet/cif/explorer/ExplorerPreChecker.java +++ b/cif/org.eclipse.escet.cif.explorer/src/org/eclipse/escet/cif/explorer/ExplorerPreChecker.java @@ -14,6 +14,10 @@ package org.eclipse.escet.cif.explorer; import org.eclipse.escet.cif.checkers.CifPreconditionChecker; +import org.eclipse.escet.cif.checkers.checks.FuncNoSpecificStdLibCheck; +import org.eclipse.escet.cif.checkers.checks.FuncNoSpecificStdLibCheck.NoSpecificStdLib; +import org.eclipse.escet.cif.checkers.checks.TypeNoSpecificTypesCheck; +import org.eclipse.escet.cif.checkers.checks.TypeNoSpecificTypesCheck.NoSpecificType; import org.eclipse.escet.common.java.Termination; /** CIF explorer precondition checker. */ @@ -24,7 +28,11 @@ public class ExplorerPreChecker extends CifPreconditionChecker { * @param termination Cooperative termination query function. */ public ExplorerPreChecker(Termination termination) { - super(termination + super(termination, + + // No distributions. + new FuncNoSpecificStdLibCheck(NoSpecificStdLib.ALL_STOCHASTIC), + new TypeNoSpecificTypesCheck(NoSpecificType.DIST_TYPES) ); } @@ -88,12 +96,6 @@ public class ExplorerPreChecker extends CifPreconditionChecker { // } // // @Override -// protected void preprocessDistType(DistType tp) { -// String msg = fmt("Distribution type \"%s\" is not supported.", CifTextUtils.typeToStr(tp)); -// problems.add(msg); -// } -// -// @Override // protected void preprocessAutomaton(Automaton aut) { // String msg; // @@ -241,13 +243,4 @@ public class ExplorerPreChecker extends CifPreconditionChecker { // problems.add(msg); // } // } -// -// @Override -// protected void preprocessStdLibFunctionExpression(StdLibFunctionExpression expr) { -// if (CifTypeUtils.isDistFunction(expr.getFunction())) { -// String msg = fmt("Distribution standard library function \"%s\" is not supported.", -// CifTextUtils.functionToStr(expr.getFunction())); -// problems.add(msg); -// } -// } } -- GitLab From d9a6f1d06b7c9ccbd8cea87442460707b6976201 Mon Sep 17 00:00:00 2001 From: Dennis Hendriks <dh_tue@hotmail.com> Date: Fri, 26 Jul 2024 14:18:50 +0200 Subject: [PATCH 04/16] #424 ExprNoSpecificExprsCheck: allow disallowing derivatives. --- .../checks/ExprNoSpecificExprsCheck.java | 7 ++- ...prNoSpecificExprsCheckLevel3.cif.check.err | 61 +++++++++++-------- 2 files changed, 40 insertions(+), 28 deletions(-) diff --git a/cif/org.eclipse.escet.cif.checkers/src/org/eclipse/escet/cif/checkers/checks/ExprNoSpecificExprsCheck.java b/cif/org.eclipse.escet.cif.checkers/src/org/eclipse/escet/cif/checkers/checks/ExprNoSpecificExprsCheck.java index 29348d0052..88bf343272 100644 --- a/cif/org.eclipse.escet.cif.checkers/src/org/eclipse/escet/cif/checkers/checks/ExprNoSpecificExprsCheck.java +++ b/cif/org.eclipse.escet.cif.checkers/src/org/eclipse/escet/cif/checkers/checks/ExprNoSpecificExprsCheck.java @@ -374,6 +374,8 @@ public class ExprNoSpecificExprsCheck extends CifCheck { // Do the check. if (disalloweds.contains(NoSpecificExpr.CONT_VAR_REFS)) { violations.add(contRef, "A continuous variable reference is used"); + } else if (disalloweds.contains(NoSpecificExpr.CONT_VAR_DERIV_REFS) && contRef.isDerivative()) { + violations.add(contRef, "A derivative of a continuous variable is used"); } } @@ -896,9 +898,12 @@ public class ExprNoSpecificExprsCheck extends CifCheck { /** Disallow constant references. */ CONST_REFS, - /** Disallow continuous variable references. */ + /** Disallow continuous variable references (including derivatives of continuous variables). */ CONT_VAR_REFS, + /** Disallow continuous variable derivative references. */ + CONT_VAR_DERIV_REFS, + /** Disallow dictionary literals. */ DICT_LITS, diff --git a/cif/org.eclipse.escet.cif.tests/tests/checks/ExprNoSpecificExprsCheckLevel3.cif.check.err b/cif/org.eclipse.escet.cif.tests/tests/checks/ExprNoSpecificExprsCheckLevel3.cif.check.err index b67194cb3f..23ea2c5852 100644 --- a/cif/org.eclipse.escet.cif.tests/tests/checks/ExprNoSpecificExprsCheckLevel3.cif.check.err +++ b/cif/org.eclipse.escet.cif.tests/tests/checks/ExprNoSpecificExprsCheckLevel3.cif.check.err @@ -15,9 +15,9 @@ WARNING: File "checks/ExprNoSpecificExprsCheckLevel3.cif": Semantic warning at l WARNING: File "checks/ExprNoSpecificExprsCheckLevel3.cif": Semantic warning at line 346, column 3: Duplicate state invariant. ERROR: CIF checks tester failed due to unsatisfied preconditions: - -------------------------------------------- - (1/9) A cast expression from string is used. - -------------------------------------------- + --------------------------------------------- + (1/10) A cast expression from string is used. + --------------------------------------------- * In group "CAST_EXPRS_STRING_TO_BOOLEAN": - invariant not <bool>"false"; ^ @@ -28,9 +28,9 @@ ERROR: CIF checks tester failed due to unsatisfied preconditions: - invariant 1.0 = <real>"1.0"; ^ - ------------------------------------------ - (2/9) A cast expression to string is used. - ------------------------------------------ + ------------------------------------------- + (2/10) A cast expression to string is used. + ------------------------------------------- * In group "CAST_EXPRS_AUTOMATON_TO_STRING": - invariant "A" = <string>X; ^ @@ -47,9 +47,16 @@ ERROR: CIF checks tester failed due to unsatisfied preconditions: - invariant "A" = <string>self; ^ - ---------------------------------------------------- - (3/9) A standard library function reference is used. - ---------------------------------------------------- + ----------------------------------------------------- + (3/10) A derivative of a continuous variable is used. + ----------------------------------------------------- + * In group "CONT_VAR_REFS_DER": + - invariant c' = 1.0; + ^ + + ----------------------------------------------------- + (4/10) A standard library function reference is used. + ----------------------------------------------------- * In group "FUNC_CALLS": - invariant abs(1) = 1; ^ @@ -57,9 +64,9 @@ ERROR: CIF checks tester failed due to unsatisfied preconditions: - invariant abs(1) = 1; ^ - ---------------------------------------------------------------------------------- - (4/9) A switch expression is used with a ranged integer typed (part of its) value. - ---------------------------------------------------------------------------------- + ----------------------------------------------------------------------------------- + (5/10) A switch expression is used with a ranged integer typed (part of its) value. + ----------------------------------------------------------------------------------- * In invariant "SWITCH_EXPRS.SWITCH_DICT": - invariant SWITCH_DICT: switch {1: 2}: case {1: 2}: true else false end; ^ @@ -70,23 +77,23 @@ ERROR: CIF checks tester failed due to unsatisfied preconditions: - invariant SWITCH_SET: switch {1, 2}: case {1, 2}: true else false end; ^ - ------------------------------------------------------------------------------------- - (5/9) A switch expression is used with a rangeless integer typed (part of its) value. - ------------------------------------------------------------------------------------- + -------------------------------------------------------------------------------------- + (6/10) A switch expression is used with a rangeless integer typed (part of its) value. + -------------------------------------------------------------------------------------- * In invariant "SWITCH_EXPRS.SWITCH_INT_RANGELESS": - invariant SWITCH_INT_RANGELESS: switch i2: case 5: true else false end; ^ - ------------------------------------------------------------------------------- - (6/9) A switch expression is used with an array list typed (part of its) value. - ------------------------------------------------------------------------------- + -------------------------------------------------------------------------------- + (7/10) A switch expression is used with an array list typed (part of its) value. + -------------------------------------------------------------------------------- * In invariant "SWITCH_EXPRS.SWITCH_LIST_ARRAY": - invariant SWITCH_LIST_ARRAY: switch i3: case [true]: true else false end; ^ - -------------------------------------------------- - (7/9) A tuple field-projection expression is used. - -------------------------------------------------- + --------------------------------------------------- + (8/10) A tuple field-projection expression is used. + --------------------------------------------------- * In automaton "PROJECTION_EXPRS_TUPLES_FIELD": - edge tau do v[a] := v[b]; ^ ^ @@ -94,9 +101,9 @@ ERROR: CIF checks tester failed due to unsatisfied preconditions: - invariant c[a]; ^ - -------------------------------------------------- - (8/9) A tuple index-projection expression is used. - -------------------------------------------------- + --------------------------------------------------- + (9/10) A tuple index-projection expression is used. + --------------------------------------------------- * In automaton "PROJECTION_EXPRS_TUPLES_FIELD": - edge tau do v[a] := v[b]; ^ ^ @@ -115,9 +122,9 @@ ERROR: CIF checks tester failed due to unsatisfied preconditions: - invariant (true, false)[0]; ^ - ------------------------------------------------ - (9/9) A user-defined function reference is used. - ------------------------------------------------ + -------------------------------------------------- + (10/10) A user-defined function reference is used. + -------------------------------------------------- * In group "FUNC_CALLS": - invariant intF(true); ^ -- GitLab From 4d2b0ee98d5be67896fd176ace808f35bbd8c838 Mon Sep 17 00:00:00 2001 From: Dennis Hendriks <dh_tue@hotmail.com> Date: Fri, 26 Jul 2024 14:19:47 +0200 Subject: [PATCH 05/16] #424 ExplorerPreChecker: move 'no derivatives' check. --- .../escet/cif/explorer/ExplorerPreChecker.java | 15 ++++++--------- 1 file changed, 6 insertions(+), 9 deletions(-) diff --git a/cif/org.eclipse.escet.cif.explorer/src/org/eclipse/escet/cif/explorer/ExplorerPreChecker.java b/cif/org.eclipse.escet.cif.explorer/src/org/eclipse/escet/cif/explorer/ExplorerPreChecker.java index 7c0cdb2bbd..eca547e543 100644 --- a/cif/org.eclipse.escet.cif.explorer/src/org/eclipse/escet/cif/explorer/ExplorerPreChecker.java +++ b/cif/org.eclipse.escet.cif.explorer/src/org/eclipse/escet/cif/explorer/ExplorerPreChecker.java @@ -14,6 +14,8 @@ package org.eclipse.escet.cif.explorer; import org.eclipse.escet.cif.checkers.CifPreconditionChecker; +import org.eclipse.escet.cif.checkers.checks.ExprNoSpecificExprsCheck; +import org.eclipse.escet.cif.checkers.checks.ExprNoSpecificExprsCheck.NoSpecificExpr; import org.eclipse.escet.cif.checkers.checks.FuncNoSpecificStdLibCheck; import org.eclipse.escet.cif.checkers.checks.FuncNoSpecificStdLibCheck.NoSpecificStdLib; import org.eclipse.escet.cif.checkers.checks.TypeNoSpecificTypesCheck; @@ -32,7 +34,10 @@ public class ExplorerPreChecker extends CifPreconditionChecker { // No distributions. new FuncNoSpecificStdLibCheck(NoSpecificStdLib.ALL_STOCHASTIC), - new TypeNoSpecificTypesCheck(NoSpecificType.DIST_TYPES) + new TypeNoSpecificTypesCheck(NoSpecificType.DIST_TYPES), + + // No derivatives. + new ExprNoSpecificExprsCheck(NoSpecificExpr.CONT_VAR_DERIV_REFS) ); } @@ -235,12 +240,4 @@ public class ExplorerPreChecker extends CifPreconditionChecker { // break; // } // } -// -// @Override -// protected void preprocessContVariableExpression(ContVariableExpression expr) { -// if (expr.isDerivative()) { -// String msg = "Use of derivatives of continuous variables is not supported."; -// problems.add(msg); -// } -// } } -- GitLab From c799f372bf45126d9a723c53782ec92658d6353d Mon Sep 17 00:00:00 2001 From: Dennis Hendriks <dh_tue@hotmail.com> Date: Fri, 26 Jul 2024 14:21:10 +0200 Subject: [PATCH 06/16] #424 ExplorerPreChecker: move 'no external user-defined funcs' check. --- .../escet/cif/explorer/ExplorerPreChecker.java | 13 ++++++------- 1 file changed, 6 insertions(+), 7 deletions(-) diff --git a/cif/org.eclipse.escet.cif.explorer/src/org/eclipse/escet/cif/explorer/ExplorerPreChecker.java b/cif/org.eclipse.escet.cif.explorer/src/org/eclipse/escet/cif/explorer/ExplorerPreChecker.java index eca547e543..4ad032416f 100644 --- a/cif/org.eclipse.escet.cif.explorer/src/org/eclipse/escet/cif/explorer/ExplorerPreChecker.java +++ b/cif/org.eclipse.escet.cif.explorer/src/org/eclipse/escet/cif/explorer/ExplorerPreChecker.java @@ -18,6 +18,8 @@ import org.eclipse.escet.cif.checkers.checks.ExprNoSpecificExprsCheck; import org.eclipse.escet.cif.checkers.checks.ExprNoSpecificExprsCheck.NoSpecificExpr; import org.eclipse.escet.cif.checkers.checks.FuncNoSpecificStdLibCheck; import org.eclipse.escet.cif.checkers.checks.FuncNoSpecificStdLibCheck.NoSpecificStdLib; +import org.eclipse.escet.cif.checkers.checks.FuncNoSpecificUserDefCheck; +import org.eclipse.escet.cif.checkers.checks.FuncNoSpecificUserDefCheck.NoSpecificUserDefFunc; import org.eclipse.escet.cif.checkers.checks.TypeNoSpecificTypesCheck; import org.eclipse.escet.cif.checkers.checks.TypeNoSpecificTypesCheck.NoSpecificType; import org.eclipse.escet.common.java.Termination; @@ -37,7 +39,10 @@ public class ExplorerPreChecker extends CifPreconditionChecker { new TypeNoSpecificTypesCheck(NoSpecificType.DIST_TYPES), // No derivatives. - new ExprNoSpecificExprsCheck(NoSpecificExpr.CONT_VAR_DERIV_REFS) + new ExprNoSpecificExprsCheck(NoSpecificExpr.CONT_VAR_DERIV_REFS), + + // No external user-defined functions. + new FuncNoSpecificUserDefCheck(NoSpecificUserDefFunc.EXTERNAL) ); } @@ -157,12 +162,6 @@ public class ExplorerPreChecker extends CifPreconditionChecker { // } // // @Override -// protected void preprocessExternalFunction(ExternalFunction func) { -// String msg = fmt("External user-defined function \"%s\" is not supported.", CifTextUtils.getAbsName(func)); -// problems.add(msg); -// } -// -// @Override // protected void preprocessInputVariable(InputVariable var) { // String msg = fmt("Input variable \"%s\" is not supported.", CifTextUtils.getAbsName(var)); // problems.add(msg); -- GitLab From 1cc4c3ab0dae85d435aee00f7e59b51c75901e53 Mon Sep 17 00:00:00 2001 From: Dennis Hendriks <dh_tue@hotmail.com> Date: Fri, 26 Jul 2024 14:31:15 +0200 Subject: [PATCH 07/16] #424 ExplorerPreChecker: move 'no input variables' check. --- .../escet/cif/explorer/ExplorerPreChecker.java | 12 +++++------- 1 file changed, 5 insertions(+), 7 deletions(-) diff --git a/cif/org.eclipse.escet.cif.explorer/src/org/eclipse/escet/cif/explorer/ExplorerPreChecker.java b/cif/org.eclipse.escet.cif.explorer/src/org/eclipse/escet/cif/explorer/ExplorerPreChecker.java index 4ad032416f..eb90b6e4ca 100644 --- a/cif/org.eclipse.escet.cif.explorer/src/org/eclipse/escet/cif/explorer/ExplorerPreChecker.java +++ b/cif/org.eclipse.escet.cif.explorer/src/org/eclipse/escet/cif/explorer/ExplorerPreChecker.java @@ -22,6 +22,7 @@ import org.eclipse.escet.cif.checkers.checks.FuncNoSpecificUserDefCheck; import org.eclipse.escet.cif.checkers.checks.FuncNoSpecificUserDefCheck.NoSpecificUserDefFunc; import org.eclipse.escet.cif.checkers.checks.TypeNoSpecificTypesCheck; import org.eclipse.escet.cif.checkers.checks.TypeNoSpecificTypesCheck.NoSpecificType; +import org.eclipse.escet.cif.checkers.checks.VarNoInputCheck; import org.eclipse.escet.common.java.Termination; /** CIF explorer precondition checker. */ @@ -42,7 +43,10 @@ public class ExplorerPreChecker extends CifPreconditionChecker { new ExprNoSpecificExprsCheck(NoSpecificExpr.CONT_VAR_DERIV_REFS), // No external user-defined functions. - new FuncNoSpecificUserDefCheck(NoSpecificUserDefFunc.EXTERNAL) + new FuncNoSpecificUserDefCheck(NoSpecificUserDefFunc.EXTERNAL), + + // No input variables. + new VarNoInputCheck() ); } @@ -162,12 +166,6 @@ public class ExplorerPreChecker extends CifPreconditionChecker { // } // // @Override -// protected void preprocessInputVariable(InputVariable var) { -// String msg = fmt("Input variable \"%s\" is not supported.", CifTextUtils.getAbsName(var)); -// problems.add(msg); -// } -// -// @Override // protected void preprocessDiscVariable(DiscVariable var) { // // Single initial value is always OK. // if (var.getValue() == null) { -- GitLab From 766c2047eccd10f382785329d0fb2866024fc34b Mon Sep 17 00:00:00 2001 From: Dennis Hendriks <dh_tue@hotmail.com> Date: Fri, 26 Jul 2024 14:32:13 +0200 Subject: [PATCH 08/16] #424 ExplorerPreChecker: remove conditionally supported features. - Not used anywhere in the codebase. --- .../cif/explorer/ExplorerPreChecker.java | 125 ------------------ 1 file changed, 125 deletions(-) diff --git a/cif/org.eclipse.escet.cif.explorer/src/org/eclipse/escet/cif/explorer/ExplorerPreChecker.java b/cif/org.eclipse.escet.cif.explorer/src/org/eclipse/escet/cif/explorer/ExplorerPreChecker.java index eb90b6e4ca..a5deb1d631 100644 --- a/cif/org.eclipse.escet.cif.explorer/src/org/eclipse/escet/cif/explorer/ExplorerPreChecker.java +++ b/cif/org.eclipse.escet.cif.explorer/src/org/eclipse/escet/cif/explorer/ExplorerPreChecker.java @@ -54,9 +54,6 @@ public class ExplorerPreChecker extends CifPreconditionChecker { // /** Found problems in the specification. */ // private Set<String> problems = null; // -// /** Set of configurable properties to check. */ -// private final EnumSet<CheckParameters> params; -// // /** // * Constructor of the {@link ExplorerPreChecker} class. // * @@ -85,86 +82,6 @@ public class ExplorerPreChecker extends CifPreconditionChecker { // throw new UnsupportedException(msg); // } // -// /** Parameters of the explorer check process. */ -// public static enum CheckParameters { -// /** Allow 'none' invariants. */ -// ALLOW_NON_INVS, -// -// /** Allow 'supervisor' invariants. */ -// ALLOW_SUP_INVS, -// -// /** Allow 'requirement' invariants. */ -// ALLOW_REQ_INVS, -// -// /** Allow 'none' automaton. */ -// ALLOW_NON_AUT, -// -// /** Allow 'supervisor' automaton. */ -// ALLOW_SUP_AUT, -// -// /** Allow 'requirement' automaton. */ -// ALLOW_REQ_AUT, -// -// /** Allow 'tau' events. */ -// ALLOW_TAU, -// } -// -// @Override -// protected void preprocessAutomaton(Automaton aut) { -// String msg; -// -// switch (aut.getKind()) { -// case NONE: -// if (params.contains(CheckParameters.ALLOW_NON_AUT)) { -// break; -// } -// msg = fmt("Regular automaton \"%s\" is not supported.", CifTextUtils.getAbsName(aut)); -// problems.add(msg); -// break; -// -// case PLANT: -// break; // Always supported. -// -// case REQUIREMENT: -// if (params.contains(CheckParameters.ALLOW_REQ_AUT)) { -// break; -// } -// msg = fmt("Requirement automaton \"%s\" is not supported.", CifTextUtils.getAbsName(aut)); -// problems.add(msg); -// break; -// -// case SUPERVISOR: -// if (params.contains(CheckParameters.ALLOW_SUP_AUT)) { -// break; -// } -// msg = fmt("Supervisor automaton \"%s\" is not supported.", CifTextUtils.getAbsName(aut)); -// problems.add(msg); -// break; -// } -// } -// -// @Override -// protected void preprocessEdge(Edge edge) { -// if (params.contains(CheckParameters.ALLOW_TAU)) { -// return; -// } -// -// String msg; -// Location loc = (Location)edge.eContainer(); -// if (edge.getEvents().isEmpty()) { -// msg = fmt("Tau events in edges of %s are not supported.", CifTextUtils.getLocationText2(loc)); -// problems.add(msg); -// return; -// } -// for (EdgeEvent ee: edge.getEvents()) { -// if (ee.getEvent() instanceof TauExpression) { -// msg = fmt("Tau events in edges of %s are not supported.", CifTextUtils.getLocationText2(loc)); -// problems.add(msg); -// return; -// } -// } -// } -// // @Override // protected void preprocessDiscVariable(DiscVariable var) { // // Single initial value is always OK. @@ -195,46 +112,4 @@ public class ExplorerPreChecker extends CifPreconditionChecker { // CifTextUtils.getAbsName(var), CifTextUtils.typeToStr(var.getType()), cntTxt); // problems.add(msg); // } -// -// @Override -// protected void preprocessInvariant(Invariant inv) { -// EObject parent = inv.eContainer(); -// String parentTxt; -// if (parent instanceof Location) { -// parentTxt = CifTextUtils.getLocationText2((Location)parent); -// } else { -// Assert.check(parent instanceof ComplexComponent); -// parentTxt = CifTextUtils.getComponentText2((ComplexComponent)parent); -// } -// -// String msg; -// switch (inv.getSupKind()) { -// case NONE: -// if (params.contains(CheckParameters.ALLOW_NON_INVS)) { -// break; -// } -// msg = fmt("Regular invariants in %s are not supported.", parentTxt); -// problems.add(msg); -// break; -// -// case PLANT: -// break; // Always supported. -// -// case REQUIREMENT: -// if (params.contains(CheckParameters.ALLOW_REQ_INVS)) { -// break; -// } -// msg = fmt("Requirement invariants in %s are not supported.", parentTxt); -// problems.add(msg); -// break; -// -// case SUPERVISOR: -// if (params.contains(CheckParameters.ALLOW_SUP_INVS)) { -// break; -// } -// msg = fmt("Supervisor invariants in %s are not supported.", parentTxt); -// problems.add(msg); -// break; -// } -// } } -- GitLab From c9aa055da7c8ec2306cbdfdc1a03d309365a6d54 Mon Sep 17 00:00:00 2001 From: Dennis Hendriks <dh_tue@hotmail.com> Date: Fri, 26 Jul 2024 14:32:31 +0200 Subject: [PATCH 09/16] #424 ExplorerPreChecker: remove no longer needed code. --- .../cif/explorer/ExplorerPreChecker.java | 31 ------------------- 1 file changed, 31 deletions(-) diff --git a/cif/org.eclipse.escet.cif.explorer/src/org/eclipse/escet/cif/explorer/ExplorerPreChecker.java b/cif/org.eclipse.escet.cif.explorer/src/org/eclipse/escet/cif/explorer/ExplorerPreChecker.java index a5deb1d631..f3e2bd2b4e 100644 --- a/cif/org.eclipse.escet.cif.explorer/src/org/eclipse/escet/cif/explorer/ExplorerPreChecker.java +++ b/cif/org.eclipse.escet.cif.explorer/src/org/eclipse/escet/cif/explorer/ExplorerPreChecker.java @@ -51,37 +51,6 @@ public class ExplorerPreChecker extends CifPreconditionChecker { ); } -// /** Found problems in the specification. */ -// private Set<String> problems = null; -// -// /** -// * Constructor of the {@link ExplorerPreChecker} class. -// * -// * @param params Set of configurable parameters for the explorer pre-checker. -// */ -// public ExplorerPreChecker(EnumSet<CheckParameters> params) { -// this.params = params; -// } -// -// /** -// * Check the specification for the requirements. -// * -// * @param spec Specification to check. -// */ -// public void checkSpec(Specification spec) { -// problems = set(); -// walkSpecification(spec); -// -// if (problems.isEmpty()) { -// return; -// } -// -// // If we have any problems, the specification is unsupported. -// String msg = "State space exploration failed due to unsatisfied preconditions:\n - " -// + String.join("\n - ", sortedstrings(problems)); -// throw new UnsupportedException(msg); -// } -// // @Override // protected void preprocessDiscVariable(DiscVariable var) { // // Single initial value is always OK. -- GitLab From a9980cf13c61fc9ca77122e1cbb282175ff0bdaa Mon Sep 17 00:00:00 2001 From: Dennis Hendriks <dh_tue@hotmail.com> Date: Fri, 26 Jul 2024 15:22:51 +0200 Subject: [PATCH 10/16] #424 Add SpecNoTooManyPossibleInitialStatesCheck. --- ...ecNoTooManyPossibleInitialStatesCheck.java | 110 ++++++++++++++++++ ...oManyPossibleInitialStatesCheckFinite.java | 21 ++++ ...anyPossibleInitialStatesCheckInfinite.java | 21 ++++ ...NoTooManyPossibleInitialStatesCheckOK.java | 21 ++++ ...ooManyPossibleInitialStatesCheckFinite.cif | 43 +++++++ ...ibleInitialStatesCheckFinite.cif.check.err | 5 + ...ManyPossibleInitialStatesCheckInfinite.cif | 14 +++ ...leInitialStatesCheckInfinite.cif.check.err | 5 + ...cNoTooManyPossibleInitialStatesCheckOK.cif | 18 +++ 9 files changed, 258 insertions(+) create mode 100644 cif/org.eclipse.escet.cif.checkers/src/org/eclipse/escet/cif/checkers/checks/SpecNoTooManyPossibleInitialStatesCheck.java create mode 100644 cif/org.eclipse.escet.cif.tests/src-test/org/eclipse/escet/cif/tests/checkers/checks/SpecNoTooManyPossibleInitialStatesCheckFinite.java create mode 100644 cif/org.eclipse.escet.cif.tests/src-test/org/eclipse/escet/cif/tests/checkers/checks/SpecNoTooManyPossibleInitialStatesCheckInfinite.java create mode 100644 cif/org.eclipse.escet.cif.tests/src-test/org/eclipse/escet/cif/tests/checkers/checks/SpecNoTooManyPossibleInitialStatesCheckOK.java create mode 100644 cif/org.eclipse.escet.cif.tests/tests/checks/SpecNoTooManyPossibleInitialStatesCheckFinite.cif create mode 100644 cif/org.eclipse.escet.cif.tests/tests/checks/SpecNoTooManyPossibleInitialStatesCheckFinite.cif.check.err create mode 100644 cif/org.eclipse.escet.cif.tests/tests/checks/SpecNoTooManyPossibleInitialStatesCheckInfinite.cif create mode 100644 cif/org.eclipse.escet.cif.tests/tests/checks/SpecNoTooManyPossibleInitialStatesCheckInfinite.cif.check.err create mode 100644 cif/org.eclipse.escet.cif.tests/tests/checks/SpecNoTooManyPossibleInitialStatesCheckOK.cif diff --git a/cif/org.eclipse.escet.cif.checkers/src/org/eclipse/escet/cif/checkers/checks/SpecNoTooManyPossibleInitialStatesCheck.java b/cif/org.eclipse.escet.cif.checkers/src/org/eclipse/escet/cif/checkers/checks/SpecNoTooManyPossibleInitialStatesCheck.java new file mode 100644 index 0000000000..0ac3f9dfc7 --- /dev/null +++ b/cif/org.eclipse.escet.cif.checkers/src/org/eclipse/escet/cif/checkers/checks/SpecNoTooManyPossibleInitialStatesCheck.java @@ -0,0 +1,110 @@ +////////////////////////////////////////////////////////////////////////////// +// Copyright (c) 2022, 2024 Contributors to the Eclipse Foundation +// +// See the NOTICE file(s) distributed with this work for additional +// information regarding copyright ownership. +// +// This program and the accompanying materials are made available +// under the terms of the MIT License which is available at +// https://opensource.org/licenses/MIT +// +// SPDX-License-Identifier: MIT +////////////////////////////////////////////////////////////////////////////// + +package org.eclipse.escet.cif.checkers.checks; + +import org.eclipse.escet.cif.checkers.CifCheckNoCompDefInst; +import org.eclipse.escet.cif.checkers.CifCheckViolations; +import org.eclipse.escet.cif.common.CifMath; +import org.eclipse.escet.cif.common.CifValueUtils; +import org.eclipse.escet.cif.metamodel.cif.Specification; +import org.eclipse.escet.cif.metamodel.cif.automata.Automaton; +import org.eclipse.escet.cif.metamodel.cif.automata.Location; +import org.eclipse.escet.cif.metamodel.cif.declarations.DiscVariable; +import org.eclipse.escet.cif.metamodel.cif.declarations.InputVariable; +import org.eclipse.escet.cif.metamodel.cif.declarations.VariableValue; + +/** + * CIF check that disallows specifications with more than {@link Integer#MAX_VALUE} possible initial states. It + * considers discrete variables, input variables and automata. + */ +public class SpecNoTooManyPossibleInitialStatesCheck extends CifCheckNoCompDefInst { + /** The current best approximation of the number of possible initial states. */ + private double count = 1; + + /** Whether the {@link #count} is approximate. */ + private boolean isApproximate = false; + + @Override + protected void preprocessDiscVariable(DiscVariable discVar, CifCheckViolations violations) { + // Get possible number of initial values of the variable. + VariableValue varValue = discVar.getValue(); + double nrOfValues; + if (varValue == null) { + nrOfValues = 1; // Implicit default initial value. + } else if (varValue.getValues().size() >= 1) { + nrOfValues = varValue.getValues().size(); // Explicit initial values. + isApproximate = true; // Some expressions may evaluate to the same value. + } else { + nrOfValues = CifValueUtils.getPossibleValueCount(discVar.getType()); + } + + // Update possible number of initial states. + count *= nrOfValues; + } + + @Override + protected void preprocessInputVariable(InputVariable inputVar, CifCheckViolations violations) { + // Get number of possible (initial) values. + double nrOfValues = CifValueUtils.getPossibleValueCount(inputVar.getType()); + + // Update possible number of initial states. + count *= nrOfValues; + } + + @Override + protected void preprocessAutomaton(Automaton aut, CifCheckViolations violations) { + // Get possible initial locations of the automaton. + int nrOfLocs = 0; + for (Location loc: aut.getLocations()) { + // Check if for sure not an initial location. + if (loc.getInitials().isEmpty()) { + continue; + } + if (CifValueUtils.isTriviallyFalse(loc.getInitials(), true, true)) { + continue; + } + + // Check if for sure an initial location. + if (CifValueUtils.isTriviallyTrue(loc.getInitials(), true, true)) { + nrOfLocs++; + continue; + } + + // Potentially an initial location. + nrOfLocs++; + isApproximate = true; + } + + // Update possible number of initial states. + count *= nrOfLocs; + } + + @Override + protected void postprocessSpecification(Specification spec, CifCheckViolations violations) { + if (count > Integer.MAX_VALUE) { + String countTxt; + if (Double.isInfinite(count)) { + violations.add(spec, "The specification has practically infinitely many possible initial states"); + } else { + countTxt = CifMath.realToStr(count); + if (isApproximate) { + countTxt = "approximately " + countTxt; + } + violations.add(spec, + "The specification has %s possible initial states, which is more than 2,147,483,647", + countTxt); + } + } + } +} diff --git a/cif/org.eclipse.escet.cif.tests/src-test/org/eclipse/escet/cif/tests/checkers/checks/SpecNoTooManyPossibleInitialStatesCheckFinite.java b/cif/org.eclipse.escet.cif.tests/src-test/org/eclipse/escet/cif/tests/checkers/checks/SpecNoTooManyPossibleInitialStatesCheckFinite.java new file mode 100644 index 0000000000..ab3a6631f8 --- /dev/null +++ b/cif/org.eclipse.escet.cif.tests/src-test/org/eclipse/escet/cif/tests/checkers/checks/SpecNoTooManyPossibleInitialStatesCheckFinite.java @@ -0,0 +1,21 @@ +////////////////////////////////////////////////////////////////////////////// +// Copyright (c) 2022, 2024 Contributors to the Eclipse Foundation +// +// See the NOTICE file(s) distributed with this work for additional +// information regarding copyright ownership. +// +// This program and the accompanying materials are made available +// under the terms of the MIT License which is available at +// https://opensource.org/licenses/MIT +// +// SPDX-License-Identifier: MIT +////////////////////////////////////////////////////////////////////////////// + +package org.eclipse.escet.cif.tests.checkers.checks; + +import org.eclipse.escet.cif.checkers.checks.SpecNoTooManyPossibleInitialStatesCheck; + +/** {@link SpecNoTooManyPossibleInitialStatesCheck} for a specification with finitely many, but too many, states. */ +public class SpecNoTooManyPossibleInitialStatesCheckFinite extends SpecNoTooManyPossibleInitialStatesCheck { + // Nothing to override. +} diff --git a/cif/org.eclipse.escet.cif.tests/src-test/org/eclipse/escet/cif/tests/checkers/checks/SpecNoTooManyPossibleInitialStatesCheckInfinite.java b/cif/org.eclipse.escet.cif.tests/src-test/org/eclipse/escet/cif/tests/checkers/checks/SpecNoTooManyPossibleInitialStatesCheckInfinite.java new file mode 100644 index 0000000000..f69171f8f5 --- /dev/null +++ b/cif/org.eclipse.escet.cif.tests/src-test/org/eclipse/escet/cif/tests/checkers/checks/SpecNoTooManyPossibleInitialStatesCheckInfinite.java @@ -0,0 +1,21 @@ +////////////////////////////////////////////////////////////////////////////// +// Copyright (c) 2022, 2024 Contributors to the Eclipse Foundation +// +// See the NOTICE file(s) distributed with this work for additional +// information regarding copyright ownership. +// +// This program and the accompanying materials are made available +// under the terms of the MIT License which is available at +// https://opensource.org/licenses/MIT +// +// SPDX-License-Identifier: MIT +////////////////////////////////////////////////////////////////////////////// + +package org.eclipse.escet.cif.tests.checkers.checks; + +import org.eclipse.escet.cif.checkers.checks.SpecNoTooManyPossibleInitialStatesCheck; + +/** {@link SpecNoTooManyPossibleInitialStatesCheck} for a specification with infinitely many states. */ +public class SpecNoTooManyPossibleInitialStatesCheckInfinite extends SpecNoTooManyPossibleInitialStatesCheck { + // Nothing to override. +} diff --git a/cif/org.eclipse.escet.cif.tests/src-test/org/eclipse/escet/cif/tests/checkers/checks/SpecNoTooManyPossibleInitialStatesCheckOK.java b/cif/org.eclipse.escet.cif.tests/src-test/org/eclipse/escet/cif/tests/checkers/checks/SpecNoTooManyPossibleInitialStatesCheckOK.java new file mode 100644 index 0000000000..58a6c57c08 --- /dev/null +++ b/cif/org.eclipse.escet.cif.tests/src-test/org/eclipse/escet/cif/tests/checkers/checks/SpecNoTooManyPossibleInitialStatesCheckOK.java @@ -0,0 +1,21 @@ +////////////////////////////////////////////////////////////////////////////// +// Copyright (c) 2022, 2024 Contributors to the Eclipse Foundation +// +// See the NOTICE file(s) distributed with this work for additional +// information regarding copyright ownership. +// +// This program and the accompanying materials are made available +// under the terms of the MIT License which is available at +// https://opensource.org/licenses/MIT +// +// SPDX-License-Identifier: MIT +////////////////////////////////////////////////////////////////////////////// + +package org.eclipse.escet.cif.tests.checkers.checks; + +import org.eclipse.escet.cif.checkers.checks.SpecNoTooManyPossibleInitialStatesCheck; + +/** {@link SpecNoTooManyPossibleInitialStatesCheck} for a specification with not too many states. */ +public class SpecNoTooManyPossibleInitialStatesCheckOK extends SpecNoTooManyPossibleInitialStatesCheck { + // Nothing to override. +} diff --git a/cif/org.eclipse.escet.cif.tests/tests/checks/SpecNoTooManyPossibleInitialStatesCheckFinite.cif b/cif/org.eclipse.escet.cif.tests/tests/checks/SpecNoTooManyPossibleInitialStatesCheckFinite.cif new file mode 100644 index 0000000000..18adadbd3b --- /dev/null +++ b/cif/org.eclipse.escet.cif.tests/tests/checks/SpecNoTooManyPossibleInitialStatesCheckFinite.cif @@ -0,0 +1,43 @@ +////////////////////////////////////////////////////////////////////////////// +// Copyright (c) 2024 Contributors to the Eclipse Foundation +// +// See the NOTICE file(s) distributed with this work for additional +// information regarding copyright ownership. +// +// This program and the accompanying materials are made available +// under the terms of the MIT License which is available at +// https://opensource.org/licenses/MIT +// +// SPDX-License-Identifier: MIT +////////////////////////////////////////////////////////////////////////////// + +event e; + +automaton aut: + disc bool v1; // 1 + disc bool v2 = true; // * 1 = 1 + disc bool v3 in {true, false}; // * 2 = 2 + disc bool v4 in any; // * 2 = 4 + disc bool v5 in any; // * 2 = 8 + disc bool v6 in any; // * 2 = 16 + disc bool v7 in any; // * 2 = 32 + disc bool v8 in any; // * 2 = 64 + disc int[0..99] v9 in any; // * 100 = 6,400 + disc int[0..99] v10 in any; // * 100 = 64,000 + disc int[0..99] v11 in any; // * 100 = 640,000 + disc int[0..99] v12 in any; // * 100 = 6,400,000 + input bool v13; // * 2 = 12,800,000 + disc int[0..99] v14 in any; // * 100 = 1,280,000,000 + + invariant v1 and v2 and v3 and v4 and v5 and v6 and v7 and v8 and v13; + invariant v9 > 0 and v10 > 0 and v11 > 0 and v12 > 0 and v14 > 0; + + location loc1: // * 2 = 2,560,000,000 + initial; + edge e goto loc3; + + location loc2: + initial 1 = 1, 2 = 2; + + location loc3; +end diff --git a/cif/org.eclipse.escet.cif.tests/tests/checks/SpecNoTooManyPossibleInitialStatesCheckFinite.cif.check.err b/cif/org.eclipse.escet.cif.tests/tests/checks/SpecNoTooManyPossibleInitialStatesCheckFinite.cif.check.err new file mode 100644 index 0000000000..cbb6d0da48 --- /dev/null +++ b/cif/org.eclipse.escet.cif.tests/tests/checks/SpecNoTooManyPossibleInitialStatesCheckFinite.cif.check.err @@ -0,0 +1,5 @@ +ERROR: CIF checks tester failed due to unsatisfied preconditions: + + ------------------------------------------------------------------------------------------------------------ + (1/1) The specification has approximately 2.56e12 possible initial states, which is more than 2,147,483,647. + ------------------------------------------------------------------------------------------------------------ diff --git a/cif/org.eclipse.escet.cif.tests/tests/checks/SpecNoTooManyPossibleInitialStatesCheckInfinite.cif b/cif/org.eclipse.escet.cif.tests/tests/checks/SpecNoTooManyPossibleInitialStatesCheckInfinite.cif new file mode 100644 index 0000000000..138c09cfd5 --- /dev/null +++ b/cif/org.eclipse.escet.cif.tests/tests/checks/SpecNoTooManyPossibleInitialStatesCheckInfinite.cif @@ -0,0 +1,14 @@ +////////////////////////////////////////////////////////////////////////////// +// Copyright (c) 2024 Contributors to the Eclipse Foundation +// +// See the NOTICE file(s) distributed with this work for additional +// information regarding copyright ownership. +// +// This program and the accompanying materials are made available +// under the terms of the MIT License which is available at +// https://opensource.org/licenses/MIT +// +// SPDX-License-Identifier: MIT +////////////////////////////////////////////////////////////////////////////// + +input real i; diff --git a/cif/org.eclipse.escet.cif.tests/tests/checks/SpecNoTooManyPossibleInitialStatesCheckInfinite.cif.check.err b/cif/org.eclipse.escet.cif.tests/tests/checks/SpecNoTooManyPossibleInitialStatesCheckInfinite.cif.check.err new file mode 100644 index 0000000000..661e28bc91 --- /dev/null +++ b/cif/org.eclipse.escet.cif.tests/tests/checks/SpecNoTooManyPossibleInitialStatesCheckInfinite.cif.check.err @@ -0,0 +1,5 @@ +ERROR: CIF checks tester failed due to unsatisfied preconditions: + + -------------------------------------------------------------------------------- + (1/1) The specification has practically infinitely many possible initial states. + -------------------------------------------------------------------------------- diff --git a/cif/org.eclipse.escet.cif.tests/tests/checks/SpecNoTooManyPossibleInitialStatesCheckOK.cif b/cif/org.eclipse.escet.cif.tests/tests/checks/SpecNoTooManyPossibleInitialStatesCheckOK.cif new file mode 100644 index 0000000000..96c6772f0c --- /dev/null +++ b/cif/org.eclipse.escet.cif.tests/tests/checks/SpecNoTooManyPossibleInitialStatesCheckOK.cif @@ -0,0 +1,18 @@ +////////////////////////////////////////////////////////////////////////////// +// Copyright (c) 2024 Contributors to the Eclipse Foundation +// +// See the NOTICE file(s) distributed with this work for additional +// information regarding copyright ownership. +// +// This program and the accompanying materials are made available +// under the terms of the MIT License which is available at +// https://opensource.org/licenses/MIT +// +// SPDX-License-Identifier: MIT +////////////////////////////////////////////////////////////////////////////// + +enum E = L1, L2, L3; + +input bool i1; +input int[0..5] i2; +input tuple(int[3..8] a; E b) i3; -- GitLab From 8fc3f656d34bf9155d427ee689c49c3916caf2e3 Mon Sep 17 00:00:00 2001 From: Dennis Hendriks <dh_tue@hotmail.com> Date: Fri, 26 Jul 2024 15:29:18 +0200 Subject: [PATCH 11/16] #424 ExplorerPreChecker: move 'not too many initial states' check. - Check now checks states of specification, not each discrete variable. - Check now takes automata into account as well. --- .../cif/explorer/ExplorerPreChecker.java | 37 +++---------------- 1 file changed, 5 insertions(+), 32 deletions(-) diff --git a/cif/org.eclipse.escet.cif.explorer/src/org/eclipse/escet/cif/explorer/ExplorerPreChecker.java b/cif/org.eclipse.escet.cif.explorer/src/org/eclipse/escet/cif/explorer/ExplorerPreChecker.java index f3e2bd2b4e..9a501bb186 100644 --- a/cif/org.eclipse.escet.cif.explorer/src/org/eclipse/escet/cif/explorer/ExplorerPreChecker.java +++ b/cif/org.eclipse.escet.cif.explorer/src/org/eclipse/escet/cif/explorer/ExplorerPreChecker.java @@ -20,6 +20,7 @@ import org.eclipse.escet.cif.checkers.checks.FuncNoSpecificStdLibCheck; import org.eclipse.escet.cif.checkers.checks.FuncNoSpecificStdLibCheck.NoSpecificStdLib; import org.eclipse.escet.cif.checkers.checks.FuncNoSpecificUserDefCheck; import org.eclipse.escet.cif.checkers.checks.FuncNoSpecificUserDefCheck.NoSpecificUserDefFunc; +import org.eclipse.escet.cif.checkers.checks.SpecNoTooManyPossibleInitialStatesCheck; import org.eclipse.escet.cif.checkers.checks.TypeNoSpecificTypesCheck; import org.eclipse.escet.cif.checkers.checks.TypeNoSpecificTypesCheck.NoSpecificType; import org.eclipse.escet.cif.checkers.checks.VarNoInputCheck; @@ -46,39 +47,11 @@ public class ExplorerPreChecker extends CifPreconditionChecker { new FuncNoSpecificUserDefCheck(NoSpecificUserDefFunc.EXTERNAL), // No input variables. - new VarNoInputCheck() + new VarNoInputCheck(), + + // Specifications with too many potential initial states are not supported. + new SpecNoTooManyPossibleInitialStatesCheck() ); } - -// @Override -// protected void preprocessDiscVariable(DiscVariable var) { -// // Single initial value is always OK. -// if (var.getValue() == null) { -// return; -// } -// List<Expression> initVals = var.getValue().getValues(); -// if (initVals.size() == 1) { -// return; -// } -// -// // Finite number of potential initial values is always OK. -// if (!initVals.isEmpty()) { -// return; -// } -// -// // Any value in its domain. Check for finite type. That is, the number -// // of possible values must fit within the range of 'int', to ensure we -// // can store the potential values in a list. -// double cnt = CifValueUtils.getPossibleValueCount(var.getType()); -// if (cnt <= Integer.MAX_VALUE) { -// return; -// } -// -// // Unsupported type for multiple initial values. -// String cntTxt = Double.isInfinite(cnt) ? "infinite" : CifMath.realToStr(cnt); -// String msg = fmt("Discrete variable \"%s\" of type \"%s\" with %s potential initial values is not supported.", -// CifTextUtils.getAbsName(var), CifTextUtils.typeToStr(var.getType()), cntTxt); -// problems.add(msg); -// } } -- GitLab From 22f2d02eb69f36b2a5f5cd4d24874558cc2dd060 Mon Sep 17 00:00:00 2001 From: Dennis Hendriks <dh_tue@hotmail.com> Date: Fri, 26 Jul 2024 15:31:30 +0200 Subject: [PATCH 12/16] #424 ExplorerApplication: use new precondition checker. --- .../escet/cif/explorer/app/ExplorerApplication.java | 11 ++++------- 1 file changed, 4 insertions(+), 7 deletions(-) diff --git a/cif/org.eclipse.escet.cif.explorer/src/org/eclipse/escet/cif/explorer/app/ExplorerApplication.java b/cif/org.eclipse.escet.cif.explorer/src/org/eclipse/escet/cif/explorer/app/ExplorerApplication.java index af2446e4e8..2da8af3110 100644 --- a/cif/org.eclipse.escet.cif.explorer/src/org/eclipse/escet/cif/explorer/app/ExplorerApplication.java +++ b/cif/org.eclipse.escet.cif.explorer/src/org/eclipse/escet/cif/explorer/app/ExplorerApplication.java @@ -20,7 +20,6 @@ import static org.eclipse.escet.common.java.Lists.list; import static org.eclipse.escet.common.java.Strings.fmt; import java.util.ArrayDeque; -import java.util.EnumSet; import java.util.List; import java.util.Queue; @@ -34,7 +33,6 @@ import org.eclipse.escet.cif.cif2cif.RemoveIoDecls; import org.eclipse.escet.cif.cif2cif.SimplifyValuesNoRefsOptimized; import org.eclipse.escet.cif.explorer.CifAutomatonBuilder; import org.eclipse.escet.cif.explorer.ExplorerPreChecker; -import org.eclipse.escet.cif.explorer.ExplorerPreChecker.CheckParameters; import org.eclipse.escet.cif.explorer.ExplorerStateFactory; import org.eclipse.escet.cif.explorer.RequirementAsPlantChecker; import org.eclipse.escet.cif.explorer.options.AddStateAnnosOption; @@ -287,16 +285,15 @@ public class ExplorerApplication extends Application<IOutputComponent> { return 0; } - // Check specification for being supported. - EnumSet<CheckParameters> params = EnumSet.allOf(CheckParameters.class); - ExplorerPreChecker checker = new ExplorerPreChecker(params); - checker.checkSpec(spec); + // Check preconditions. + Termination termination = () -> isTerminationRequested(); + ExplorerPreChecker checker = new ExplorerPreChecker(termination); + checker.reportPreconditionViolations(spec, absSpecPath, "CIF explorer"); if (isTerminationRequested()) { return 0; } // Warn about features of the specification that may lead to an unexpected resulting state space. - Termination termination = () -> isTerminationRequested(); CifCheck[] checks = {new RequirementAsPlantChecker()}; CifCheckViolations warnings = new CifChecker(termination, checks).check(spec, absSpecPath); if (warnings.hasViolations()) { -- GitLab From 84a3268c8d50fdca0f9dd55053b17a50127711d1 Mon Sep 17 00:00:00 2001 From: Dennis Hendriks <dh_tue@hotmail.com> Date: Fri, 26 Jul 2024 15:37:04 +0200 Subject: [PATCH 13/16] #424 Update test. - Remove what is not checked. - Add what is checked but missing from the test. - Update test output. --- .../explorer/multi_init_too_many1.run.err | 6 +- .../explorer/multi_init_too_many2.run.err | 6 +- .../tests/explorer/preconditions.cif | 53 ++--------------- .../tests/explorer/preconditions.run.err | 58 ++++++++++++++----- 4 files changed, 58 insertions(+), 65 deletions(-) diff --git a/cif/org.eclipse.escet.cif.tests/tests/explorer/multi_init_too_many1.run.err b/cif/org.eclipse.escet.cif.tests/tests/explorer/multi_init_too_many1.run.err index b8b284cd89..8c8e0f3974 100644 --- a/cif/org.eclipse.escet.cif.tests/tests/explorer/multi_init_too_many1.run.err +++ b/cif/org.eclipse.escet.cif.tests/tests/explorer/multi_init_too_many1.run.err @@ -1 +1,5 @@ -ERROR: Too many potential initial states to store: 2.147483648e9. +ERROR: CIF explorer failed due to unsatisfied preconditions: + + ---------------------------------------------------------------------------------------------------- + (1/1) The specification has 2.147483648e9 possible initial states, which is more than 2,147,483,647. + ---------------------------------------------------------------------------------------------------- diff --git a/cif/org.eclipse.escet.cif.tests/tests/explorer/multi_init_too_many2.run.err b/cif/org.eclipse.escet.cif.tests/tests/explorer/multi_init_too_many2.run.err index f32d99abfd..30e1eb49ad 100644 --- a/cif/org.eclipse.escet.cif.tests/tests/explorer/multi_init_too_many2.run.err +++ b/cif/org.eclipse.escet.cif.tests/tests/explorer/multi_init_too_many2.run.err @@ -1 +1,5 @@ -ERROR: Too many potential initial states to store: 4.295098369e9. +ERROR: CIF explorer failed due to unsatisfied preconditions: + + ---------------------------------------------------------------------------------------------------- + (1/1) The specification has 4.295098369e9 possible initial states, which is more than 2,147,483,647. + ---------------------------------------------------------------------------------------------------- diff --git a/cif/org.eclipse.escet.cif.tests/tests/explorer/preconditions.cif b/cif/org.eclipse.escet.cif.tests/tests/explorer/preconditions.cif index 801c783d80..9be4d6882a 100644 --- a/cif/org.eclipse.escet.cif.tests/tests/explorer/preconditions.cif +++ b/cif/org.eclipse.escet.cif.tests/tests/explorer/preconditions.cif @@ -15,60 +15,17 @@ plant pp: disc dist real d = constant(1.0); // Distribution stdlib function. alg real x = (sample d)[0]; // Sampling. - disc int d1 in any; // Multiple potential initial values. - disc list string d2 in any; // Multiple potential initial values. + disc int d1 in any; // Too many potential initial values. + disc list string d2 in any; // Too many potential initial values. initial d1 = size(d2); // Silence unused warnings. location: initial; end +cont c der 1; +invariant c' = 0; // Derivative reference. + func int f(): "java:some.Class.Method"; // External user-defined function. input bool i; // Input variable. - -// Not yet included in this test as default state explorer allows them: -plant b: - location a: - initial; - edge when true; // Implicit tau. - - location b: - initial; - edge tau; // Explicit tau. -end - - invariant false; // Regular invariant. -plant invariant false; -requirement invariant false; // Requirement invariant. -supervisor invariant false; // Supervisor invariant. - -automaton aa: - location: - initial; - - invariant false; // Regular invariant. - plant invariant false; - requirement invariant false; // Requirement invariant. - supervisor invariant false; // Supervisor invariant. -end - -automaton a: // Regular automaton. - location: - initial; -end - -plant p: - location: - initial; -end - -requirement r: // Requirement automaton. - location: - initial; -end - -supervisor s: // Supervisor automaton. - location: - initial; -end diff --git a/cif/org.eclipse.escet.cif.tests/tests/explorer/preconditions.run.err b/cif/org.eclipse.escet.cif.tests/tests/explorer/preconditions.run.err index f31af31bf8..de31884dd3 100644 --- a/cif/org.eclipse.escet.cif.tests/tests/explorer/preconditions.run.err +++ b/cif/org.eclipse.escet.cif.tests/tests/explorer/preconditions.run.err @@ -1,15 +1,43 @@ -WARNING: File "explorer/preconditions.cif": Semantic warning at line 41, column 13: Duplicate state invariant. -WARNING: File "explorer/preconditions.cif": Semantic warning at line 42, column 13: Duplicate state invariant. -WARNING: File "explorer/preconditions.cif": Semantic warning at line 43, column 13: Duplicate state invariant. -WARNING: File "explorer/preconditions.cif": Semantic warning at line 44, column 13: Duplicate state invariant. -WARNING: File "explorer/preconditions.cif": Semantic warning at line 50, column 17: Duplicate state invariant. -WARNING: File "explorer/preconditions.cif": Semantic warning at line 51, column 17: Duplicate state invariant. -WARNING: File "explorer/preconditions.cif": Semantic warning at line 52, column 17: Duplicate state invariant. -WARNING: File "explorer/preconditions.cif": Semantic warning at line 53, column 17: Duplicate state invariant. -ERROR: State space exploration failed due to unsatisfied preconditions: - - Discrete variable "pp.d1" of type "int" with 4.294967296e9 potential initial values is not supported. - - Discrete variable "pp.d2" of type "list string" with infinite potential initial values is not supported. - - Distribution standard library function "constant" is not supported. - - Distribution type "dist real" is not supported. - - External user-defined function "f" is not supported. - - Input variable "i" is not supported. +ERROR: CIF explorer failed due to unsatisfied preconditions: + + ---------------------------------------------------- + (1/6) A derivative of a continuous variable is used. + ---------------------------------------------------- + * In the top-level scope of the specification: + - invariant c' = 0.0; + ^ + + ---------------------------------- + (2/6) A distribution type is used. + ---------------------------------- + * In discrete variable "pp.d": + - disc dist real d = constant(1.0); + ^ ^ ^ + * In algebraic variable "pp.x": + - alg real x = (sample d)[0]; + ^ ^ + + ---------------------------------------------------- + (3/6) Function is an external user-defined function. + ---------------------------------------------------- + * In the top-level scope of the specification: + - func int f(): "java:some.Class.Method"; + ^ + + --------------------------------------------------- + (4/6) Standard library function "constant" is used. + --------------------------------------------------- + * In discrete variable "pp.d": + - disc dist real d = constant(1.0); + ^ + + -------------------------------------------------------------------------------- + (5/6) The specification has practically infinitely many possible initial states. + -------------------------------------------------------------------------------- + + ------------------------------------ + (6/6) Variable is an input variable. + ------------------------------------ + * In the top-level scope of the specification: + - input bool i; + ^ -- GitLab From 3c7de23680f13ad061e88a2b9f1aeea09de81c97 Mon Sep 17 00:00:00 2001 From: Dennis Hendriks <dh_tue@hotmail.com> Date: Fri, 26 Jul 2024 15:46:56 +0200 Subject: [PATCH 14/16] #424 ExplorerApplication: reorder methods in invocation order. - Only reordered. No other changes. --- .../cif/explorer/app/ExplorerApplication.java | 208 +++++++++--------- 1 file changed, 104 insertions(+), 104 deletions(-) diff --git a/cif/org.eclipse.escet.cif.explorer/src/org/eclipse/escet/cif/explorer/app/ExplorerApplication.java b/cif/org.eclipse.escet.cif.explorer/src/org/eclipse/escet/cif/explorer/app/ExplorerApplication.java index 2da8af3110..92054fc1a4 100644 --- a/cif/org.eclipse.escet.cif.explorer/src/org/eclipse/escet/cif/explorer/app/ExplorerApplication.java +++ b/cif/org.eclipse.escet.cif.explorer/src/org/eclipse/escet/cif/explorer/app/ExplorerApplication.java @@ -94,8 +94,108 @@ public class ExplorerApplication extends Application<IOutputComponent> { } @Override - protected OutputProvider<IOutputComponent> getProvider() { - return new OutputProvider<>(); + public String getAppName() { + return "CIF untimed state space explorer"; + } + + @Override + public String getAppDescription() { + return "Explore a CIF specification to its untimed state space."; + } + + @Override + protected int runInternal() { + // Read CIF file. + CifReader cifReader = new CifReader().init(); + Specification spec = cifReader.read(); + String absSpecPath = Paths.resolve(InputFileOption.getPath()); + if (isTerminationRequested()) { + return 0; + } + + // Remove/ignore I/O declarations, to increase the supported subset. + RemoveIoDecls removeIoDecls = new RemoveIoDecls(); + removeIoDecls.transform(spec); + if (removeIoDecls.haveAnySvgInputDeclarationsBeenRemoved()) { + warn("The specification contains CIF/SVG input declarations. These will be ignored."); + } + + // Perform preprocessing. For value simplification, constants are + // not inlined, and the optimized variant is used for performance + // reasons. + new RemoveAnnotations().transform(spec); + new ElimComponentDefInst().transform(spec); + new ElimSelf().transform(spec); + new SimplifyValuesNoRefsOptimized().transform(spec); + if (isTerminationRequested()) { + return 0; + } + + // Check preconditions. + Termination termination = () -> isTerminationRequested(); + ExplorerPreChecker checker = new ExplorerPreChecker(termination); + checker.reportPreconditionViolations(spec, absSpecPath, "CIF explorer"); + if (isTerminationRequested()) { + return 0; + } + + // Warn about features of the specification that may lead to an unexpected resulting state space. + CifCheck[] checks = {new RequirementAsPlantChecker()}; + CifCheckViolations warnings = new CifChecker(termination, checks).check(spec, absSpecPath); + if (warnings.hasViolations()) { + String incompleteTxt = ""; + if (warnings.isIncomplete()) { + incompleteTxt = " (checking was prematurely terminated, so the report below may be incomplete)"; + } + warn(String.join("\n", + concat(fmt( + "The CIF specification has features that may cause an unexpected resulting state space%s:", + incompleteTxt), warnings.createReport()))); + } + if (isTerminationRequested()) { + return 0; + } + + // Explore the state space. + Explorer e; + try { + ExplorerBuilder builder = new ExplorerBuilder(spec); + builder.collectData(); + e = builder.buildExplorer(new ExplorerStateFactory()); + explore(e); + } catch (ExplorationTerminatedException ex) { + return 0; + } + if (isTerminationRequested()) { + return 0; + } + + // Remove duplicate transitions of the state space, if requested. + if (RemoveDuplicateTransitionsOption.isEnabled()) { + e.removeDuplicateTransitions(); + } + if (isTerminationRequested()) { + return 0; + } + + // Write output. + writeStatisticsOutput(e); + if (isTerminationRequested()) { + return 0; + } + + writeReportOutput(e); + if (isTerminationRequested()) { + return 0; + } + + writeAutomatonOutput(e, spec, cifReader.getAbsDirPath(), "statespace"); + if (isTerminationRequested()) { + return 0; + } + + // Done. + return 0; } /** @@ -258,108 +358,8 @@ public class ExplorerApplication extends Application<IOutputComponent> { } @Override - protected int runInternal() { - // Read CIF file. - CifReader cifReader = new CifReader().init(); - Specification spec = cifReader.read(); - String absSpecPath = Paths.resolve(InputFileOption.getPath()); - if (isTerminationRequested()) { - return 0; - } - - // Remove/ignore I/O declarations, to increase the supported subset. - RemoveIoDecls removeIoDecls = new RemoveIoDecls(); - removeIoDecls.transform(spec); - if (removeIoDecls.haveAnySvgInputDeclarationsBeenRemoved()) { - warn("The specification contains CIF/SVG input declarations. These will be ignored."); - } - - // Perform preprocessing. For value simplification, constants are - // not inlined, and the optimized variant is used for performance - // reasons. - new RemoveAnnotations().transform(spec); - new ElimComponentDefInst().transform(spec); - new ElimSelf().transform(spec); - new SimplifyValuesNoRefsOptimized().transform(spec); - if (isTerminationRequested()) { - return 0; - } - - // Check preconditions. - Termination termination = () -> isTerminationRequested(); - ExplorerPreChecker checker = new ExplorerPreChecker(termination); - checker.reportPreconditionViolations(spec, absSpecPath, "CIF explorer"); - if (isTerminationRequested()) { - return 0; - } - - // Warn about features of the specification that may lead to an unexpected resulting state space. - CifCheck[] checks = {new RequirementAsPlantChecker()}; - CifCheckViolations warnings = new CifChecker(termination, checks).check(spec, absSpecPath); - if (warnings.hasViolations()) { - String incompleteTxt = ""; - if (warnings.isIncomplete()) { - incompleteTxt = " (checking was prematurely terminated, so the report below may be incomplete)"; - } - warn(String.join("\n", - concat(fmt( - "The CIF specification has features that may cause an unexpected resulting state space%s:", - incompleteTxt), warnings.createReport()))); - } - if (isTerminationRequested()) { - return 0; - } - - // Explore the state space. - Explorer e; - try { - ExplorerBuilder builder = new ExplorerBuilder(spec); - builder.collectData(); - e = builder.buildExplorer(new ExplorerStateFactory()); - explore(e); - } catch (ExplorationTerminatedException ex) { - return 0; - } - if (isTerminationRequested()) { - return 0; - } - - // Remove duplicate transitions of the state space, if requested. - if (RemoveDuplicateTransitionsOption.isEnabled()) { - e.removeDuplicateTransitions(); - } - if (isTerminationRequested()) { - return 0; - } - - // Write output. - writeStatisticsOutput(e); - if (isTerminationRequested()) { - return 0; - } - - writeReportOutput(e); - if (isTerminationRequested()) { - return 0; - } - - writeAutomatonOutput(e, spec, cifReader.getAbsDirPath(), "statespace"); - if (isTerminationRequested()) { - return 0; - } - - // Done. - return 0; - } - - @Override - public String getAppName() { - return "CIF untimed state space explorer"; - } - - @Override - public String getAppDescription() { - return "Explore a CIF specification to its untimed state space."; + protected OutputProvider<IOutputComponent> getProvider() { + return new OutputProvider<>(); } /** -- GitLab From fb02ef18a5c43de46280db1f731eebcd954f2f0f Mon Sep 17 00:00:00 2001 From: Dennis Hendriks <dh_tue@hotmail.com> Date: Mon, 29 Jul 2024 10:44:39 +0200 Subject: [PATCH 15/16] #424 ExporerApplication: move getAppName/Description back down. --- .../cif/explorer/app/ExplorerApplication.java | 20 +++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) diff --git a/cif/org.eclipse.escet.cif.explorer/src/org/eclipse/escet/cif/explorer/app/ExplorerApplication.java b/cif/org.eclipse.escet.cif.explorer/src/org/eclipse/escet/cif/explorer/app/ExplorerApplication.java index 92054fc1a4..e0747b9088 100644 --- a/cif/org.eclipse.escet.cif.explorer/src/org/eclipse/escet/cif/explorer/app/ExplorerApplication.java +++ b/cif/org.eclipse.escet.cif.explorer/src/org/eclipse/escet/cif/explorer/app/ExplorerApplication.java @@ -93,16 +93,6 @@ public class ExplorerApplication extends Application<IOutputComponent> { super(streams); } - @Override - public String getAppName() { - return "CIF untimed state space explorer"; - } - - @Override - public String getAppDescription() { - return "Explore a CIF specification to its untimed state space."; - } - @Override protected int runInternal() { // Read CIF file. @@ -357,6 +347,16 @@ public class ExplorerApplication extends Application<IOutputComponent> { CifWriter.writeCifSpec(spec, new PathPair(path, absPath), specPath); } + @Override + public String getAppName() { + return "CIF untimed state space explorer"; + } + + @Override + public String getAppDescription() { + return "Explore a CIF specification to its untimed state space."; + } + @Override protected OutputProvider<IOutputComponent> getProvider() { return new OutputProvider<>(); -- GitLab From 3f807c05ecef9ecdf0866106a9a08a6ee1c4e088 Mon Sep 17 00:00:00 2001 From: Dennis Hendriks <dh_tue@hotmail.com> Date: Mon, 29 Jul 2024 16:38:44 +0200 Subject: [PATCH 16/16] #424 Improve a check violation message. --- .../checks/SpecNoTooManyPossibleInitialStatesCheck.java | 2 +- ...cNoTooManyPossibleInitialStatesCheckFinite.cif.check.err | 6 +++--- .../tests/explorer/multi_init_too_many1.run.err | 6 +++--- .../tests/explorer/multi_init_too_many2.run.err | 6 +++--- 4 files changed, 10 insertions(+), 10 deletions(-) diff --git a/cif/org.eclipse.escet.cif.checkers/src/org/eclipse/escet/cif/checkers/checks/SpecNoTooManyPossibleInitialStatesCheck.java b/cif/org.eclipse.escet.cif.checkers/src/org/eclipse/escet/cif/checkers/checks/SpecNoTooManyPossibleInitialStatesCheck.java index 0ac3f9dfc7..61b922ee7a 100644 --- a/cif/org.eclipse.escet.cif.checkers/src/org/eclipse/escet/cif/checkers/checks/SpecNoTooManyPossibleInitialStatesCheck.java +++ b/cif/org.eclipse.escet.cif.checkers/src/org/eclipse/escet/cif/checkers/checks/SpecNoTooManyPossibleInitialStatesCheck.java @@ -102,7 +102,7 @@ public class SpecNoTooManyPossibleInitialStatesCheck extends CifCheckNoCompDefIn countTxt = "approximately " + countTxt; } violations.add(spec, - "The specification has %s possible initial states, which is more than 2,147,483,647", + "The specification has %s possible initial states, more than the maximum of 2,147,483,647", countTxt); } } diff --git a/cif/org.eclipse.escet.cif.tests/tests/checks/SpecNoTooManyPossibleInitialStatesCheckFinite.cif.check.err b/cif/org.eclipse.escet.cif.tests/tests/checks/SpecNoTooManyPossibleInitialStatesCheckFinite.cif.check.err index cbb6d0da48..0648daa0ce 100644 --- a/cif/org.eclipse.escet.cif.tests/tests/checks/SpecNoTooManyPossibleInitialStatesCheckFinite.cif.check.err +++ b/cif/org.eclipse.escet.cif.tests/tests/checks/SpecNoTooManyPossibleInitialStatesCheckFinite.cif.check.err @@ -1,5 +1,5 @@ ERROR: CIF checks tester failed due to unsatisfied preconditions: - ------------------------------------------------------------------------------------------------------------ - (1/1) The specification has approximately 2.56e12 possible initial states, which is more than 2,147,483,647. - ------------------------------------------------------------------------------------------------------------ + ------------------------------------------------------------------------------------------------------------------ + (1/1) The specification has approximately 2.56e12 possible initial states, more than the maximum of 2,147,483,647. + ------------------------------------------------------------------------------------------------------------------ diff --git a/cif/org.eclipse.escet.cif.tests/tests/explorer/multi_init_too_many1.run.err b/cif/org.eclipse.escet.cif.tests/tests/explorer/multi_init_too_many1.run.err index 8c8e0f3974..a28b5ee26f 100644 --- a/cif/org.eclipse.escet.cif.tests/tests/explorer/multi_init_too_many1.run.err +++ b/cif/org.eclipse.escet.cif.tests/tests/explorer/multi_init_too_many1.run.err @@ -1,5 +1,5 @@ ERROR: CIF explorer failed due to unsatisfied preconditions: - ---------------------------------------------------------------------------------------------------- - (1/1) The specification has 2.147483648e9 possible initial states, which is more than 2,147,483,647. - ---------------------------------------------------------------------------------------------------- + ---------------------------------------------------------------------------------------------------------- + (1/1) The specification has 2.147483648e9 possible initial states, more than the maximum of 2,147,483,647. + ---------------------------------------------------------------------------------------------------------- diff --git a/cif/org.eclipse.escet.cif.tests/tests/explorer/multi_init_too_many2.run.err b/cif/org.eclipse.escet.cif.tests/tests/explorer/multi_init_too_many2.run.err index 30e1eb49ad..578312d429 100644 --- a/cif/org.eclipse.escet.cif.tests/tests/explorer/multi_init_too_many2.run.err +++ b/cif/org.eclipse.escet.cif.tests/tests/explorer/multi_init_too_many2.run.err @@ -1,5 +1,5 @@ ERROR: CIF explorer failed due to unsatisfied preconditions: - ---------------------------------------------------------------------------------------------------- - (1/1) The specification has 4.295098369e9 possible initial states, which is more than 2,147,483,647. - ---------------------------------------------------------------------------------------------------- + ---------------------------------------------------------------------------------------------------------- + (1/1) The specification has 4.295098369e9 possible initial states, more than the maximum of 2,147,483,647. + ---------------------------------------------------------------------------------------------------------- -- GitLab