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