From 40f6822c178cbaa36222b56b971c666d33cfffc2 Mon Sep 17 00:00:00 2001 From: Dennis Hendriks <dh_tue@hotmail.com> Date: Fri, 26 Jul 2024 11:28:30 +0200 Subject: [PATCH 01/20] #424 CIF to mCRL2 precond chk: add new class. No checks for now. --- .../META-INF/MANIFEST.MF | 3 +- .../cif/cif2mcrl2/CifToMcrl2PreChecker.java | 31 +++++++++++++++++++ 2 files changed, 33 insertions(+), 1 deletion(-) create mode 100644 cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java diff --git a/cif/org.eclipse.escet.cif.cif2mcrl2/META-INF/MANIFEST.MF b/cif/org.eclipse.escet.cif.cif2mcrl2/META-INF/MANIFEST.MF index f19987d34c..3672a29105 100644 --- a/cif/org.eclipse.escet.cif.cif2mcrl2/META-INF/MANIFEST.MF +++ b/cif/org.eclipse.escet.cif.cif2mcrl2/META-INF/MANIFEST.MF @@ -20,7 +20,8 @@ Require-Bundle: org.eclipse.ui;bundle-version="3.115.0", org.eclipse.escet.cif.metamodel.java;bundle-version="5.0.0", org.eclipse.escet.cif.common;bundle-version="5.0.0", org.apache.commons.lang3;bundle-version="3.1.0", - org.eclipse.escet.common.box;bundle-version="5.0.0" + org.eclipse.escet.common.box;bundle-version="5.0.0", + org.eclipse.escet.cif.checkers;bundle-version="5.0.0" Import-Package: org.junit.jupiter.api;version="5.9.2" Bundle-RequiredExecutionEnvironment: JavaSE-17 Bundle-ActivationPolicy: lazy diff --git a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java new file mode 100644 index 0000000000..968f093926 --- /dev/null +++ b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java @@ -0,0 +1,31 @@ +////////////////////////////////////////////////////////////////////////////// +// Copyright (c) 2010, 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.cif2mcrl2; + +import org.eclipse.escet.cif.checkers.CifPreconditionChecker; +import org.eclipse.escet.common.java.Termination; + +/** CIF to mCRL2 transformation precondition checker. */ +public class CifToMcrl2PreChecker extends CifPreconditionChecker { + /** + * Constructor for the {@link CifToMcrl2PreChecker} class. + * + * @param termination Cooperative termination query function. + */ + public CifToMcrl2PreChecker(Termination termination) { + super(termination + + ); + } +} -- GitLab From 1fe87739162da2d7fb06e9a58760e3b4574d8308 Mon Sep 17 00:00:00 2001 From: Dennis Hendriks <dh_tue@hotmail.com> Date: Fri, 26 Jul 2024 11:41:58 +0200 Subject: [PATCH 02/20] #424 CIF to mCRL2 preconds move: only bool/int/enum types. --- .../escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java | 9 --------- .../cif/cif2mcrl2/CifToMcrl2PreChecker.java | 16 +++++++++++++++- 2 files changed, 15 insertions(+), 10 deletions(-) diff --git a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java index 9401ab118e..13d9748eee 100644 --- a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java +++ b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java @@ -144,13 +144,6 @@ public class Cif2Mcrl2PreChecker { for (Declaration decl: aut.getDeclarations()) { if (decl instanceof DiscVariable) { DiscVariable dv = (DiscVariable)decl; - CifType tp = CifTypeUtils.normalizeType(dv.getType()); - if (!(tp instanceof BoolType) && !(tp instanceof IntType) && !(tp instanceof EnumType)) { - msg = fmt("Discrete variable \"%s\" does not have a boolean, integer, or enumeration type.", - CifTextUtils.getAbsName(dv)); - problems.add(msg); - continue; - } if (dv.getValue().getValues().size() != 1) { msg = fmt("Discrete variable \"%s\" does not have a single initial value.", @@ -362,8 +355,6 @@ public class Cif2Mcrl2PreChecker { return fmt("has unsupported enumeration expression \"%s\".", CifTextUtils.exprToStr(e)); } - String msg = CifTextUtils.typeToStr(t); - return fmt("has an unsupported type \"%s\" in expression \"%s\".", msg, CifTextUtils.exprToStr(e)); } /** diff --git a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java index 968f093926..ca251e933b 100644 --- a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java +++ b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java @@ -14,6 +14,8 @@ package org.eclipse.escet.cif.cif2mcrl2; import org.eclipse.escet.cif.checkers.CifPreconditionChecker; +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 to mCRL2 transformation precondition checker. */ @@ -24,7 +26,19 @@ public class CifToMcrl2PreChecker extends CifPreconditionChecker { * @param termination Cooperative termination query function. */ public CifToMcrl2PreChecker(Termination termination) { - super(termination + super(termination, + + // Only boolean, integer and enumeration types are supported. + new TypeNoSpecificTypesCheck( + NoSpecificType.COMP_TYPES, + NoSpecificType.DICT_TYPES, + NoSpecificType.DIST_TYPES, + NoSpecificType.FUNC_TYPES, + NoSpecificType.LIST_TYPES, + NoSpecificType.REAL_TYPES, + NoSpecificType.SET_TYPES, + NoSpecificType.STRING_TYPES, + NoSpecificType.TUPLE_TYPES) ); } -- GitLab From d362543c7ea0174c93ec78b7618f57d9cfacb230 Mon Sep 17 00:00:00 2001 From: Dennis Hendriks <dh_tue@hotmail.com> Date: Fri, 26 Jul 2024 11:44:19 +0200 Subject: [PATCH 03/20] #424 CIF to mCRL2 preconds move: disc var at most one initial value. --- .../eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java | 7 ------- .../eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java | 6 +++++- 2 files changed, 5 insertions(+), 8 deletions(-) diff --git a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java index 13d9748eee..6756620894 100644 --- a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java +++ b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java @@ -145,13 +145,6 @@ public class Cif2Mcrl2PreChecker { if (decl instanceof DiscVariable) { DiscVariable dv = (DiscVariable)decl; - if (dv.getValue().getValues().size() != 1) { - msg = fmt("Discrete variable \"%s\" does not have a single initial value.", - CifTextUtils.getAbsName(dv)); - problems.add(msg); - continue; - } - try { CifEvalUtils.eval(dv.getValue().getValues().get(0), true); } catch (CifEvalException err) { diff --git a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java index ca251e933b..b38d8a7d3e 100644 --- a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java +++ b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java @@ -16,6 +16,7 @@ package org.eclipse.escet.cif.cif2mcrl2; import org.eclipse.escet.cif.checkers.CifPreconditionChecker; import org.eclipse.escet.cif.checkers.checks.TypeNoSpecificTypesCheck; import org.eclipse.escet.cif.checkers.checks.TypeNoSpecificTypesCheck.NoSpecificType; +import org.eclipse.escet.cif.checkers.checks.VarNoDiscWithMultiInitValuesCheck; import org.eclipse.escet.common.java.Termination; /** CIF to mCRL2 transformation precondition checker. */ @@ -38,7 +39,10 @@ public class CifToMcrl2PreChecker extends CifPreconditionChecker { NoSpecificType.REAL_TYPES, NoSpecificType.SET_TYPES, NoSpecificType.STRING_TYPES, - NoSpecificType.TUPLE_TYPES) + NoSpecificType.TUPLE_TYPES), + + // Discrete variables must not have multiple potential initial values. + new VarNoDiscWithMultiInitValuesCheck() ); } -- GitLab From 6bfe3b514401f8b9e57209ee956b16e62d9d6ecb Mon Sep 17 00:00:00 2001 From: Dennis Hendriks <dh_tue@hotmail.com> Date: Fri, 26 Jul 2024 11:46:41 +0200 Subject: [PATCH 04/20] #424 CIF to mCRL2 preconds move: disc var initial value static eval. --- .../escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java | 16 ---------------- .../cif/cif2mcrl2/CifToMcrl2PreChecker.java | 6 +++++- 2 files changed, 5 insertions(+), 17 deletions(-) diff --git a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java index 6756620894..c3f15d58c5 100644 --- a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java +++ b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java @@ -140,22 +140,6 @@ public class Cif2Mcrl2PreChecker { checkComponent(aut); - // Check type of the discrete variables. Only support Boolean, (ranged) integer and enumeration types. - for (Declaration decl: aut.getDeclarations()) { - if (decl instanceof DiscVariable) { - DiscVariable dv = (DiscVariable)decl; - - try { - CifEvalUtils.eval(dv.getValue().getValues().get(0), true); - } catch (CifEvalException err) { - msg = fmt("Initial value of discrete variable \"%s\" cannot be evaluated.", - CifTextUtils.getAbsName(dv)); - problems.add(msg); - continue; - } - } - } - // Check locations. for (Location loc: aut.getLocations()) { String locTextMid = CifTextUtils.getLocationText2(loc); diff --git a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java index b38d8a7d3e..c2451b2c33 100644 --- a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java +++ b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java @@ -16,6 +16,7 @@ package org.eclipse.escet.cif.cif2mcrl2; import org.eclipse.escet.cif.checkers.CifPreconditionChecker; import org.eclipse.escet.cif.checkers.checks.TypeNoSpecificTypesCheck; import org.eclipse.escet.cif.checkers.checks.TypeNoSpecificTypesCheck.NoSpecificType; +import org.eclipse.escet.cif.checkers.checks.VarDiscOnlyStaticEvalInitCheck; import org.eclipse.escet.cif.checkers.checks.VarNoDiscWithMultiInitValuesCheck; import org.eclipse.escet.common.java.Termination; @@ -42,7 +43,10 @@ public class CifToMcrl2PreChecker extends CifPreconditionChecker { NoSpecificType.TUPLE_TYPES), // Discrete variables must not have multiple potential initial values. - new VarNoDiscWithMultiInitValuesCheck() + new VarNoDiscWithMultiInitValuesCheck(), + + // Initial values of discrete variables must be statically evaluable. + new VarDiscOnlyStaticEvalInitCheck() ); } -- GitLab From 3c37b062baee1ea02969eeded511e23b7fdd7d99 Mon Sep 17 00:00:00 2001 From: Dennis Hendriks <dh_tue@hotmail.com> Date: Fri, 26 Jul 2024 11:48:07 +0200 Subject: [PATCH 05/20] #424 CIF to mCRL2 preconds move: no continuous variables. --- .../eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java | 6 ------ .../eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java | 6 +++++- 2 files changed, 5 insertions(+), 7 deletions(-) diff --git a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java index c3f15d58c5..1427a9b467 100644 --- a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java +++ b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java @@ -40,7 +40,6 @@ import org.eclipse.escet.cif.metamodel.cif.automata.Location; import org.eclipse.escet.cif.metamodel.cif.automata.Update; import org.eclipse.escet.cif.metamodel.cif.declarations.AlgVariable; import org.eclipse.escet.cif.metamodel.cif.declarations.Constant; -import org.eclipse.escet.cif.metamodel.cif.declarations.ContVariable; import org.eclipse.escet.cif.metamodel.cif.declarations.Declaration; import org.eclipse.escet.cif.metamodel.cif.declarations.DiscVariable; import org.eclipse.escet.cif.metamodel.cif.declarations.EnumDecl; @@ -351,11 +350,6 @@ public class Cif2Mcrl2PreChecker { continue; } else if (decl instanceof Event) { continue; - } else if (decl instanceof ContVariable) { - msg = fmt("Continuous variable \"%s\" is unsupported in the transformation.", - CifTextUtils.getAbsName(decl)); - problems.add(msg); - continue; } else if (decl instanceof Function) { continue; } else if (decl instanceof TypeDecl) { diff --git a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java index c2451b2c33..10203a762f 100644 --- a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java +++ b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java @@ -17,6 +17,7 @@ import org.eclipse.escet.cif.checkers.CifPreconditionChecker; import org.eclipse.escet.cif.checkers.checks.TypeNoSpecificTypesCheck; import org.eclipse.escet.cif.checkers.checks.TypeNoSpecificTypesCheck.NoSpecificType; import org.eclipse.escet.cif.checkers.checks.VarDiscOnlyStaticEvalInitCheck; +import org.eclipse.escet.cif.checkers.checks.VarNoContinuousCheck; import org.eclipse.escet.cif.checkers.checks.VarNoDiscWithMultiInitValuesCheck; import org.eclipse.escet.common.java.Termination; @@ -46,7 +47,10 @@ public class CifToMcrl2PreChecker extends CifPreconditionChecker { new VarNoDiscWithMultiInitValuesCheck(), // Initial values of discrete variables must be statically evaluable. - new VarDiscOnlyStaticEvalInitCheck() + new VarDiscOnlyStaticEvalInitCheck(), + + // Continuous variables are not supported. + new VarNoContinuousCheck() ); } -- GitLab From 15f224ade6a8391bfa52f1adc94798083c3c6713 Mon Sep 17 00:00:00 2001 From: Dennis Hendriks <dh_tue@hotmail.com> Date: Fri, 26 Jul 2024 11:49:46 +0200 Subject: [PATCH 06/20] #424 CIF to mCRL2 preconds move: no input variables. --- .../cif/cif2mcrl2/Cif2Mcrl2PreChecker.java | 36 ------------------- .../cif/cif2mcrl2/CifToMcrl2PreChecker.java | 6 +++- 2 files changed, 5 insertions(+), 37 deletions(-) diff --git a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java index 1427a9b467..d500a193d7 100644 --- a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java +++ b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java @@ -44,7 +44,6 @@ import org.eclipse.escet.cif.metamodel.cif.declarations.Declaration; import org.eclipse.escet.cif.metamodel.cif.declarations.DiscVariable; import org.eclipse.escet.cif.metamodel.cif.declarations.EnumDecl; import org.eclipse.escet.cif.metamodel.cif.declarations.Event; -import org.eclipse.escet.cif.metamodel.cif.declarations.InputVariable; import org.eclipse.escet.cif.metamodel.cif.declarations.TypeDecl; import org.eclipse.escet.cif.metamodel.cif.expressions.BinaryExpression; import org.eclipse.escet.cif.metamodel.cif.expressions.BoolExpression; @@ -333,39 +332,6 @@ public class Cif2Mcrl2PreChecker { } - /** - * Check that only supported declarations exist. - * - * @param decls Declarations to inspect. - */ - private void checkDeclarations(List<Declaration> decls) { - String msg; - - for (Declaration decl: decls) { - if (decl instanceof AlgVariable) { - // Eliminated during preprocessing. - } else if (decl instanceof Constant) { - // Eliminated during preprocessing. - } else if (decl instanceof EnumDecl) { - continue; - } else if (decl instanceof Event) { - continue; - } else if (decl instanceof Function) { - continue; - } else if (decl instanceof TypeDecl) { - continue; - } else if (decl instanceof DiscVariable) { - continue; - } else if (decl instanceof InputVariable) { - msg = fmt("Input variable \"%s\" is unsupported in the transformation.", CifTextUtils.getAbsName(decl)); - problems.add(msg); - continue; - } - - throw new RuntimeException("Unexpected type of CIF declaration."); - } - } - /** * Verify that the given component does not have elements that are not supported in the translation. * @@ -377,8 +343,6 @@ public class Cif2Mcrl2PreChecker { // IO declarations should be eliminated already. Assert.check(comp.getIoDecls().isEmpty()); - checkDeclarations(comp.getDeclarations()); - if (!comp.getEquations().isEmpty()) { msg = fmt("Equations are not supported in %s.", CifTextUtils.getComponentText2(comp)); problems.add(msg); diff --git a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java index 10203a762f..f025cc5452 100644 --- a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java +++ b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java @@ -19,6 +19,7 @@ import org.eclipse.escet.cif.checkers.checks.TypeNoSpecificTypesCheck.NoSpecific import org.eclipse.escet.cif.checkers.checks.VarDiscOnlyStaticEvalInitCheck; import org.eclipse.escet.cif.checkers.checks.VarNoContinuousCheck; import org.eclipse.escet.cif.checkers.checks.VarNoDiscWithMultiInitValuesCheck; +import org.eclipse.escet.cif.checkers.checks.VarNoInputCheck; import org.eclipse.escet.common.java.Termination; /** CIF to mCRL2 transformation precondition checker. */ @@ -50,7 +51,10 @@ public class CifToMcrl2PreChecker extends CifPreconditionChecker { new VarDiscOnlyStaticEvalInitCheck(), // Continuous variables are not supported. - new VarNoContinuousCheck() + new VarNoContinuousCheck(), + + // Input variables are not supported. + new VarNoInputCheck() ); } -- GitLab From 1ad27018e82e7adf88dd7bb2bf47a54b689664c1 Mon Sep 17 00:00:00 2001 From: Dennis Hendriks <dh_tue@hotmail.com> Date: Fri, 26 Jul 2024 11:50:43 +0200 Subject: [PATCH 07/20] #424 CIF to mCRL2 preconds move: no equations. --- .../cif/cif2mcrl2/Cif2Mcrl2PreChecker.java | 18 ------------------ .../cif/cif2mcrl2/CifToMcrl2PreChecker.java | 6 +++++- 2 files changed, 5 insertions(+), 19 deletions(-) diff --git a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java index d500a193d7..ce87d3e5d0 100644 --- a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java +++ b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java @@ -20,8 +20,6 @@ import java.util.Collections; import java.util.List; import org.apache.commons.lang3.StringUtils; -import org.eclipse.escet.cif.common.CifEvalException; -import org.eclipse.escet.cif.common.CifEvalUtils; import org.eclipse.escet.cif.common.CifTextUtils; import org.eclipse.escet.cif.common.CifTypeUtils; import org.eclipse.escet.cif.common.CifValueUtils; @@ -38,13 +36,6 @@ import org.eclipse.escet.cif.metamodel.cif.automata.EdgeSend; import org.eclipse.escet.cif.metamodel.cif.automata.IfUpdate; import org.eclipse.escet.cif.metamodel.cif.automata.Location; import org.eclipse.escet.cif.metamodel.cif.automata.Update; -import org.eclipse.escet.cif.metamodel.cif.declarations.AlgVariable; -import org.eclipse.escet.cif.metamodel.cif.declarations.Constant; -import org.eclipse.escet.cif.metamodel.cif.declarations.Declaration; -import org.eclipse.escet.cif.metamodel.cif.declarations.DiscVariable; -import org.eclipse.escet.cif.metamodel.cif.declarations.EnumDecl; -import org.eclipse.escet.cif.metamodel.cif.declarations.Event; -import org.eclipse.escet.cif.metamodel.cif.declarations.TypeDecl; import org.eclipse.escet.cif.metamodel.cif.expressions.BinaryExpression; import org.eclipse.escet.cif.metamodel.cif.expressions.BoolExpression; import org.eclipse.escet.cif.metamodel.cif.expressions.DiscVariableExpression; @@ -54,7 +45,6 @@ import org.eclipse.escet.cif.metamodel.cif.expressions.Expression; import org.eclipse.escet.cif.metamodel.cif.expressions.IntExpression; import org.eclipse.escet.cif.metamodel.cif.expressions.TauExpression; import org.eclipse.escet.cif.metamodel.cif.expressions.UnaryExpression; -import org.eclipse.escet.cif.metamodel.cif.functions.Function; import org.eclipse.escet.cif.metamodel.cif.types.BoolType; import org.eclipse.escet.cif.metamodel.cif.types.CifType; import org.eclipse.escet.cif.metamodel.cif.types.EnumType; @@ -147,10 +137,6 @@ public class Cif2Mcrl2PreChecker { msg = locTextStart + " has invariants."; problems.add(msg); } - if (!loc.getEquations().isEmpty()) { - msg = locTextStart + " has equations."; - problems.add(msg); - } for (Edge edge: loc.getEdges()) { for (Update upd: edge.getUpdates()) { if (upd instanceof IfUpdate) { @@ -343,10 +329,6 @@ public class Cif2Mcrl2PreChecker { // IO declarations should be eliminated already. Assert.check(comp.getIoDecls().isEmpty()); - if (!comp.getEquations().isEmpty()) { - msg = fmt("Equations are not supported in %s.", CifTextUtils.getComponentText2(comp)); - problems.add(msg); - } if (!comp.getInitials().isEmpty()) { msg = fmt("Initialization predicates are not supported in %s.", CifTextUtils.getComponentText2(comp)); problems.add(msg); diff --git a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java index f025cc5452..4dc2c9b71b 100644 --- a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java +++ b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java @@ -14,6 +14,7 @@ package org.eclipse.escet.cif.cif2mcrl2; import org.eclipse.escet.cif.checkers.CifPreconditionChecker; +import org.eclipse.escet.cif.checkers.checks.EqnNotAllowedCheck; import org.eclipse.escet.cif.checkers.checks.TypeNoSpecificTypesCheck; import org.eclipse.escet.cif.checkers.checks.TypeNoSpecificTypesCheck.NoSpecificType; import org.eclipse.escet.cif.checkers.checks.VarDiscOnlyStaticEvalInitCheck; @@ -54,7 +55,10 @@ public class CifToMcrl2PreChecker extends CifPreconditionChecker { new VarNoContinuousCheck(), // Input variables are not supported. - new VarNoInputCheck() + new VarNoInputCheck(), + + // Equations are not supported. + new EqnNotAllowedCheck() ); } -- GitLab From f507877f7ff998aaaf759155273aa1429addd668 Mon Sep 17 00:00:00 2001 From: Dennis Hendriks <dh_tue@hotmail.com> Date: Fri, 26 Jul 2024 11:52:34 +0200 Subject: [PATCH 08/20] #424 CIF to mCRL2 preconds move: no channels. --- .../escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java | 12 +----------- .../escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java | 6 +++++- 2 files changed, 6 insertions(+), 12 deletions(-) diff --git a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java index ce87d3e5d0..36ad71f453 100644 --- a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java +++ b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java @@ -31,8 +31,6 @@ import org.eclipse.escet.cif.metamodel.cif.automata.Assignment; 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.EdgeReceive; -import org.eclipse.escet.cif.metamodel.cif.automata.EdgeSend; import org.eclipse.escet.cif.metamodel.cif.automata.IfUpdate; import org.eclipse.escet.cif.metamodel.cif.automata.Location; import org.eclipse.escet.cif.metamodel.cif.automata.Update; @@ -173,15 +171,7 @@ public class Cif2Mcrl2PreChecker { continue; } for (EdgeEvent ee: edge.getEvents()) { - if (ee instanceof EdgeSend) { - msg = locTextStart + " has a send edge."; - problems.add(msg); - continue; - } else if (ee instanceof EdgeReceive) { - msg = locTextStart + " has a receive edge."; - problems.add(msg); - continue; - } else if (ee.getEvent() instanceof TauExpression) { + if (ee.getEvent() instanceof TauExpression) { msg = locTextStart + " has a \"tau\" event."; problems.add(msg); continue; diff --git a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java index 4dc2c9b71b..efa873e175 100644 --- a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java +++ b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java @@ -15,6 +15,7 @@ package org.eclipse.escet.cif.cif2mcrl2; import org.eclipse.escet.cif.checkers.CifPreconditionChecker; import org.eclipse.escet.cif.checkers.checks.EqnNotAllowedCheck; +import org.eclipse.escet.cif.checkers.checks.EventNoChannelsCheck; import org.eclipse.escet.cif.checkers.checks.TypeNoSpecificTypesCheck; import org.eclipse.escet.cif.checkers.checks.TypeNoSpecificTypesCheck.NoSpecificType; import org.eclipse.escet.cif.checkers.checks.VarDiscOnlyStaticEvalInitCheck; @@ -58,7 +59,10 @@ public class CifToMcrl2PreChecker extends CifPreconditionChecker { new VarNoInputCheck(), // Equations are not supported. - new EqnNotAllowedCheck() + new EqnNotAllowedCheck(), + + // Channels are not supported. + new EventNoChannelsCheck() ); } -- GitLab From f2060f2d6f82a6788b3a1ac1381e9e0b28d7de6c Mon Sep 17 00:00:00 2001 From: Dennis Hendriks <dh_tue@hotmail.com> Date: Fri, 26 Jul 2024 11:53:34 +0200 Subject: [PATCH 09/20] #424 CIF to mCRL2 preconds move: no tau. --- .../cif/cif2mcrl2/Cif2Mcrl2PreChecker.java | 17 ----------------- .../cif/cif2mcrl2/CifToMcrl2PreChecker.java | 6 +++++- 2 files changed, 5 insertions(+), 18 deletions(-) diff --git a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java index 36ad71f453..4c81c30278 100644 --- a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java +++ b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java @@ -30,7 +30,6 @@ import org.eclipse.escet.cif.metamodel.cif.Specification; import org.eclipse.escet.cif.metamodel.cif.automata.Assignment; 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.IfUpdate; import org.eclipse.escet.cif.metamodel.cif.automata.Location; import org.eclipse.escet.cif.metamodel.cif.automata.Update; @@ -38,10 +37,8 @@ import org.eclipse.escet.cif.metamodel.cif.expressions.BinaryExpression; import org.eclipse.escet.cif.metamodel.cif.expressions.BoolExpression; import org.eclipse.escet.cif.metamodel.cif.expressions.DiscVariableExpression; import org.eclipse.escet.cif.metamodel.cif.expressions.EnumLiteralExpression; -import org.eclipse.escet.cif.metamodel.cif.expressions.EventExpression; import org.eclipse.escet.cif.metamodel.cif.expressions.Expression; import org.eclipse.escet.cif.metamodel.cif.expressions.IntExpression; -import org.eclipse.escet.cif.metamodel.cif.expressions.TauExpression; import org.eclipse.escet.cif.metamodel.cif.expressions.UnaryExpression; import org.eclipse.escet.cif.metamodel.cif.types.BoolType; import org.eclipse.escet.cif.metamodel.cif.types.CifType; @@ -164,20 +161,6 @@ public class Cif2Mcrl2PreChecker { problems.add(msg); } } - - if (edge.getEvents().isEmpty()) { - msg = locTextStart + " has a \"tau\" event."; - problems.add(msg); - continue; - } - for (EdgeEvent ee: edge.getEvents()) { - if (ee.getEvent() instanceof TauExpression) { - msg = locTextStart + " has a \"tau\" event."; - problems.add(msg); - continue; - } - Assert.check(ee.getEvent() instanceof EventExpression); - } } } diff --git a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java index efa873e175..4f5b232149 100644 --- a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java +++ b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java @@ -16,6 +16,7 @@ package org.eclipse.escet.cif.cif2mcrl2; import org.eclipse.escet.cif.checkers.CifPreconditionChecker; import org.eclipse.escet.cif.checkers.checks.EqnNotAllowedCheck; import org.eclipse.escet.cif.checkers.checks.EventNoChannelsCheck; +import org.eclipse.escet.cif.checkers.checks.EventNoTauCheck; import org.eclipse.escet.cif.checkers.checks.TypeNoSpecificTypesCheck; import org.eclipse.escet.cif.checkers.checks.TypeNoSpecificTypesCheck.NoSpecificType; import org.eclipse.escet.cif.checkers.checks.VarDiscOnlyStaticEvalInitCheck; @@ -62,7 +63,10 @@ public class CifToMcrl2PreChecker extends CifPreconditionChecker { new EqnNotAllowedCheck(), // Channels are not supported. - new EventNoChannelsCheck() + new EventNoChannelsCheck(), + + // 'Tau' events are not supported. + new EventNoTauCheck() ); } -- GitLab From 8528a199f356e0ec7e3e425fdf61100d4305cd34 Mon Sep 17 00:00:00 2001 From: Dennis Hendriks <dh_tue@hotmail.com> Date: Fri, 26 Jul 2024 11:56:13 +0200 Subject: [PATCH 10/20] #424 CIF to mCRL2 preconds move: at least one automaton. --- .../escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java | 12 +++--------- .../escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java | 6 +++++- 2 files changed, 8 insertions(+), 10 deletions(-) diff --git a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java index 4c81c30278..d895133836 100644 --- a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java +++ b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java @@ -67,9 +67,7 @@ public class Cif2Mcrl2PreChecker { */ public void checkSpec(Specification spec) { problems = list(); - if (!checkGroup(spec)) { - problems.add("Specification must have at least one automaton."); - } + checkGroup(spec); if (problems.isEmpty()) { return; @@ -87,30 +85,26 @@ public class Cif2Mcrl2PreChecker { * Unfold and check a group. * * @param grp Group to check and unfold. - * @return Whether at least one automaton was found in the group. */ - private boolean checkGroup(Group grp) { + private void checkGroup(Group grp) { // Definitions should be eliminated already. Assert.check(grp.getDefinitions().isEmpty()); checkComponent(grp); - boolean foundAut = false; for (Component c: grp.getComponents()) { if (c instanceof Automaton) { - foundAut = true; Automaton aut = (Automaton)c; checkAutomaton(aut); continue; } else if (c instanceof Group) { Group g = (Group)c; - foundAut |= checkGroup(g); + checkGroup(g); continue; } // ComponentInst should not happen, as DefInst has been eliminated. throw new RuntimeException("Unexpected type of Component."); } - return foundAut; } /** diff --git a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java index 4f5b232149..c6820f8bcd 100644 --- a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java +++ b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java @@ -17,6 +17,7 @@ import org.eclipse.escet.cif.checkers.CifPreconditionChecker; import org.eclipse.escet.cif.checkers.checks.EqnNotAllowedCheck; import org.eclipse.escet.cif.checkers.checks.EventNoChannelsCheck; import org.eclipse.escet.cif.checkers.checks.EventNoTauCheck; +import org.eclipse.escet.cif.checkers.checks.SpecAutomataCountsCheck; import org.eclipse.escet.cif.checkers.checks.TypeNoSpecificTypesCheck; import org.eclipse.escet.cif.checkers.checks.TypeNoSpecificTypesCheck.NoSpecificType; import org.eclipse.escet.cif.checkers.checks.VarDiscOnlyStaticEvalInitCheck; @@ -66,7 +67,10 @@ public class CifToMcrl2PreChecker extends CifPreconditionChecker { new EventNoChannelsCheck(), // 'Tau' events are not supported. - new EventNoTauCheck() + new EventNoTauCheck(), + + // There must be at least one automaton. + new SpecAutomataCountsCheck().setMinMaxAuts(1, SpecAutomataCountsCheck.NO_CHANGE) ); } -- GitLab From 03c3e86fd49fad439dec9039434e6742b05db33c Mon Sep 17 00:00:00 2001 From: Dennis Hendriks <dh_tue@hotmail.com> Date: Fri, 26 Jul 2024 11:59:09 +0200 Subject: [PATCH 11/20] #424 CIF to mCRL2 preconds move: automata exactly one initial location. --- .../cif/cif2mcrl2/Cif2Mcrl2PreChecker.java | 19 ------------------- .../cif/cif2mcrl2/CifToMcrl2PreChecker.java | 6 +++++- 2 files changed, 5 insertions(+), 20 deletions(-) diff --git a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java index d895133836..0dc82136a5 100644 --- a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java +++ b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java @@ -22,7 +22,6 @@ import java.util.List; import org.apache.commons.lang3.StringUtils; 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.Component; import org.eclipse.escet.cif.metamodel.cif.Group; @@ -157,24 +156,6 @@ public class Cif2Mcrl2PreChecker { } } } - - // Check the number of initial locations. - int initLocCount = 0; - for (Location loc: aut.getLocations()) { - if (!loc.getInitials().isEmpty() && CifValueUtils.isTriviallyTrue(loc.getInitials(), true, true)) { - initLocCount++; - } - } - - if (initLocCount == 0) { - msg = fmt("Automaton \"%s\" has no initial location.", CifTextUtils.getAbsName(aut)); - problems.add(msg); - } - - if (initLocCount > 1) { - msg = fmt("Automaton \"%s\" has more than one initial location.", CifTextUtils.getAbsName(aut)); - problems.add(msg); - } } /** diff --git a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java index c6820f8bcd..803cd602ba 100644 --- a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java +++ b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java @@ -14,6 +14,7 @@ package org.eclipse.escet.cif.cif2mcrl2; import org.eclipse.escet.cif.checkers.CifPreconditionChecker; +import org.eclipse.escet.cif.checkers.checks.AutOnlyWithOneInitLocCheck; import org.eclipse.escet.cif.checkers.checks.EqnNotAllowedCheck; import org.eclipse.escet.cif.checkers.checks.EventNoChannelsCheck; import org.eclipse.escet.cif.checkers.checks.EventNoTauCheck; @@ -70,7 +71,10 @@ public class CifToMcrl2PreChecker extends CifPreconditionChecker { new EventNoTauCheck(), // There must be at least one automaton. - new SpecAutomataCountsCheck().setMinMaxAuts(1, SpecAutomataCountsCheck.NO_CHANGE) + new SpecAutomataCountsCheck().setMinMaxAuts(1, SpecAutomataCountsCheck.NO_CHANGE), + + // Exactly one initial location per automaton. + new AutOnlyWithOneInitLocCheck() ); } -- GitLab From db0f8d5798e69b68e8c5cf24fd6e434f147f4341 Mon Sep 17 00:00:00 2001 From: Dennis Hendriks <dh_tue@hotmail.com> Date: Fri, 26 Jul 2024 12:01:15 +0200 Subject: [PATCH 12/20] #424 CIF to mCRL2 preconds move: only simple assignments. --- .../escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java | 14 -------------- .../escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java | 6 +++++- 2 files changed, 5 insertions(+), 15 deletions(-) diff --git a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java index 0dc82136a5..5a46919398 100644 --- a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java +++ b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java @@ -29,7 +29,6 @@ import org.eclipse.escet.cif.metamodel.cif.Specification; import org.eclipse.escet.cif.metamodel.cif.automata.Assignment; 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.IfUpdate; import org.eclipse.escet.cif.metamodel.cif.automata.Location; import org.eclipse.escet.cif.metamodel.cif.automata.Update; import org.eclipse.escet.cif.metamodel.cif.expressions.BinaryExpression; @@ -127,25 +126,12 @@ public class Cif2Mcrl2PreChecker { } for (Edge edge: loc.getEdges()) { for (Update upd: edge.getUpdates()) { - if (upd instanceof IfUpdate) { - msg = locTextStart + " has conditional updates."; - problems.add(msg); - continue; - } - Assignment asg = (Assignment)upd; msg = checkExpression(asg.getValue()); if (msg != null) { msg = fmt("A value in %s %s", locTextMid, msg); problems.add(msg); } - - Expression e = asg.getAddressable(); - if (!(e instanceof DiscVariableExpression)) { - msg = fmt("An assignment in %s assigns to unsupported addressable form \"%s\".", locTextMid, - CifTextUtils.exprToStr(e)); - problems.add(msg); - } } for (Expression e: edge.getGuards()) { msg = checkExpression(e); diff --git a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java index 803cd602ba..ca318839b8 100644 --- a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java +++ b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java @@ -15,6 +15,7 @@ package org.eclipse.escet.cif.cif2mcrl2; import org.eclipse.escet.cif.checkers.CifPreconditionChecker; import org.eclipse.escet.cif.checkers.checks.AutOnlyWithOneInitLocCheck; +import org.eclipse.escet.cif.checkers.checks.EdgeOnlySimpleAssignmentsCheck; import org.eclipse.escet.cif.checkers.checks.EqnNotAllowedCheck; import org.eclipse.escet.cif.checkers.checks.EventNoChannelsCheck; import org.eclipse.escet.cif.checkers.checks.EventNoTauCheck; @@ -74,7 +75,10 @@ public class CifToMcrl2PreChecker extends CifPreconditionChecker { new SpecAutomataCountsCheck().setMinMaxAuts(1, SpecAutomataCountsCheck.NO_CHANGE), // Exactly one initial location per automaton. - new AutOnlyWithOneInitLocCheck() + new AutOnlyWithOneInitLocCheck(), + + // No conditional updates and multi-assignments. + new EdgeOnlySimpleAssignmentsCheck() ); } -- GitLab From a6278446492c97f17a6ff6f03e42a2a817006d1a Mon Sep 17 00:00:00 2001 From: Dennis Hendriks <dh_tue@hotmail.com> Date: Fri, 26 Jul 2024 12:37:07 +0200 Subject: [PATCH 13/20] #424 CIF to mCRL2 preconds move: only supported expressions. --- .../cif/cif2mcrl2/Cif2Mcrl2PreChecker.java | 140 ------------------ .../cif/cif2mcrl2/CifToMcrl2PreChecker.java | 77 +++++++++- 2 files changed, 76 insertions(+), 141 deletions(-) diff --git a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java index 5a46919398..a52e396637 100644 --- a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java +++ b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java @@ -21,27 +21,12 @@ import java.util.List; import org.apache.commons.lang3.StringUtils; import org.eclipse.escet.cif.common.CifTextUtils; -import org.eclipse.escet.cif.common.CifTypeUtils; import org.eclipse.escet.cif.metamodel.cif.ComplexComponent; import org.eclipse.escet.cif.metamodel.cif.Component; import org.eclipse.escet.cif.metamodel.cif.Group; import org.eclipse.escet.cif.metamodel.cif.Specification; -import org.eclipse.escet.cif.metamodel.cif.automata.Assignment; 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.Location; -import org.eclipse.escet.cif.metamodel.cif.automata.Update; -import org.eclipse.escet.cif.metamodel.cif.expressions.BinaryExpression; -import org.eclipse.escet.cif.metamodel.cif.expressions.BoolExpression; -import org.eclipse.escet.cif.metamodel.cif.expressions.DiscVariableExpression; -import org.eclipse.escet.cif.metamodel.cif.expressions.EnumLiteralExpression; -import org.eclipse.escet.cif.metamodel.cif.expressions.Expression; -import org.eclipse.escet.cif.metamodel.cif.expressions.IntExpression; -import org.eclipse.escet.cif.metamodel.cif.expressions.UnaryExpression; -import org.eclipse.escet.cif.metamodel.cif.types.BoolType; -import org.eclipse.escet.cif.metamodel.cif.types.CifType; -import org.eclipse.escet.cif.metamodel.cif.types.EnumType; -import org.eclipse.escet.cif.metamodel.cif.types.IntType; import org.eclipse.escet.common.java.Assert; import org.eclipse.escet.common.java.Strings; import org.eclipse.escet.common.java.exceptions.InvalidInputException; @@ -124,132 +109,7 @@ public class Cif2Mcrl2PreChecker { msg = locTextStart + " has invariants."; problems.add(msg); } - for (Edge edge: loc.getEdges()) { - for (Update upd: edge.getUpdates()) { - Assignment asg = (Assignment)upd; - msg = checkExpression(asg.getValue()); - if (msg != null) { - msg = fmt("A value in %s %s", locTextMid, msg); - problems.add(msg); - } - } - for (Expression e: edge.getGuards()) { - msg = checkExpression(e); - if (msg != null) { - msg = fmt("A guard in %s %s", locTextMid, msg); - problems.add(msg); - } - } - } - } - } - - /** - * Check whether the expression supported. - * - * @param e Expression to check. - * @return The last part of an error message if an error was found, else {@code null}. - */ - private String checkExpression(Expression e) { - CifType t = CifTypeUtils.normalizeType(e.getType()); - - if (t instanceof BoolType) { - if (e instanceof BoolExpression) { - return null; - } else if (e instanceof BinaryExpression) { - BinaryExpression be = (BinaryExpression)e; - switch (be.getOperator()) { - case CONJUNCTION: - case DISJUNCTION: - case EQUAL: - case GREATER_EQUAL: - case GREATER_THAN: - case LESS_EQUAL: - case LESS_THAN: - case UNEQUAL: - case IMPLICATION: - break; - default: { - String msg = fmt("has unsupported boolean binary operator \"%s\".", - CifTextUtils.operatorToStr(be.getOperator())); - return msg; - } - } - String msg = checkExpression(be.getLeft()); - if (msg == null) { - msg = checkExpression(be.getRight()); - } - return msg; - } else if (e instanceof UnaryExpression) { - UnaryExpression ue = (UnaryExpression)e; - switch (ue.getOperator()) { - case INVERSE: - break; - default: { - String msg = fmt("has unsupported boolean unary operator \"%s\".", - CifTextUtils.operatorToStr(ue.getOperator())); - return msg; - } - } - return checkExpression(ue.getChild()); - } else if (e instanceof DiscVariableExpression) { - return null; - } - - return fmt("has unsupported boolean expression \"%s\".", CifTextUtils.exprToStr(e)); } - - if (t instanceof IntType) { - if (e instanceof IntExpression) { - return null; - } else if (e instanceof BinaryExpression) { - BinaryExpression be = (BinaryExpression)e; - switch (be.getOperator()) { - case ADDITION: - case MULTIPLICATION: - case SUBTRACTION: - break; - default: { - String msg = fmt("has unsupported integer binary operator \"%s\".", - CifTextUtils.operatorToStr(be.getOperator())); - return msg; - } - } - String msg = checkExpression(be.getLeft()); - if (msg == null) { - msg = checkExpression(be.getRight()); - } - return msg; - } else if (e instanceof UnaryExpression) { - UnaryExpression ue = (UnaryExpression)e; - switch (ue.getOperator()) { - case NEGATE: - case PLUS: - break; - default: { - String msg = fmt("has unsupported integer unary operator \"%s\".", - CifTextUtils.operatorToStr(ue.getOperator())); - return msg; - } - } - return checkExpression(ue.getChild()); - } else if (e instanceof DiscVariableExpression) { - return null; - } - - return fmt("has unsupported integer expression \"%s\".", CifTextUtils.exprToStr(e)); - } - - if (t instanceof EnumType) { - if (e instanceof EnumLiteralExpression) { - return null; - } else if (e instanceof DiscVariableExpression) { - return null; - } - - return fmt("has unsupported enumeration expression \"%s\".", CifTextUtils.exprToStr(e)); - } - } /** diff --git a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java index ca318839b8..2a962188c1 100644 --- a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java +++ b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java @@ -19,6 +19,12 @@ import org.eclipse.escet.cif.checkers.checks.EdgeOnlySimpleAssignmentsCheck; import org.eclipse.escet.cif.checkers.checks.EqnNotAllowedCheck; import org.eclipse.escet.cif.checkers.checks.EventNoChannelsCheck; import org.eclipse.escet.cif.checkers.checks.EventNoTauCheck; +import org.eclipse.escet.cif.checkers.checks.ExprNoSpecificBinaryExprsCheck; +import org.eclipse.escet.cif.checkers.checks.ExprNoSpecificBinaryExprsCheck.NoSpecificBinaryOp; +import org.eclipse.escet.cif.checkers.checks.ExprNoSpecificExprsCheck; +import org.eclipse.escet.cif.checkers.checks.ExprNoSpecificExprsCheck.NoSpecificExpr; +import org.eclipse.escet.cif.checkers.checks.ExprNoSpecificUnaryExprsCheck; +import org.eclipse.escet.cif.checkers.checks.ExprNoSpecificUnaryExprsCheck.NoSpecificUnaryOp; import org.eclipse.escet.cif.checkers.checks.SpecAutomataCountsCheck; import org.eclipse.escet.cif.checkers.checks.TypeNoSpecificTypesCheck; import org.eclipse.escet.cif.checkers.checks.TypeNoSpecificTypesCheck.NoSpecificType; @@ -78,7 +84,76 @@ public class CifToMcrl2PreChecker extends CifPreconditionChecker { new AutOnlyWithOneInitLocCheck(), // No conditional updates and multi-assignments. - new EdgeOnlySimpleAssignmentsCheck() + new EdgeOnlySimpleAssignmentsCheck(), + + // Only certain expression: + // - For expressions that produce a boolean value, only boolean literals, constants (eliminated + // already), discrete variables, algebraic variables (eliminated already), binary operators 'and', + // 'or', '=>', '=', '!=', '<', '<=', '>' and '>=', and unary operator 'not' are supported. + // - For expressions that produce an enumeration value, only enumeration literals, constants (eliminated + // already), discrete variables, and algebraic variables (eliminated already) are supported. + // - For expressions that produce an integer value, only integer literals, constants (eliminated + // already), discrete variables, algebraic variables (eliminated already), binary operators '+', '*' + // and '-', and unary operators '-' and '+' are supported. + // - Unary and binary expressions are only supported with boolean, integer and enumeration operands. + new ExprNoSpecificExprsCheck( + NoSpecificExpr.FUNC_REFS, + NoSpecificExpr.CAST_EXPRS, + NoSpecificExpr.COMP_REFS, + NoSpecificExpr.CONT_VAR_REFS, + NoSpecificExpr.DICT_LITS, + NoSpecificExpr.TUPLE_FIELD_REFS, + NoSpecificExpr.FUNC_CALLS, + NoSpecificExpr.IF_EXPRS, + NoSpecificExpr.INPUT_VAR_REFS, + NoSpecificExpr.LIST_LITS, + NoSpecificExpr.LOC_REFS, + NoSpecificExpr.PROJECTION_EXPRS, + NoSpecificExpr.REAL_LITS, + NoSpecificExpr.RECEIVE_EXPRS, + NoSpecificExpr.SET_LITS, + NoSpecificExpr.SLICE_EXPRS, + NoSpecificExpr.STRING_LITS, + NoSpecificExpr.SWITCH_EXPRS, + NoSpecificExpr.TIME_VAR_REFS, + NoSpecificExpr.TUPLE_LITS), + new ExprNoSpecificBinaryExprsCheck( + NoSpecificBinaryOp.ADDITION_REALS, + NoSpecificBinaryOp.ADDITION_LISTS, + NoSpecificBinaryOp.ADDITION_STRINGS, + NoSpecificBinaryOp.ADDITION_DICTS, + NoSpecificBinaryOp.CONJUNCTION_SETS, + NoSpecificBinaryOp.DISJUNCTION_SETS, + NoSpecificBinaryOp.DIVISION, + NoSpecificBinaryOp.ELEMENT_OF, + NoSpecificBinaryOp.EQUAL_DICT, + NoSpecificBinaryOp.EQUAL_LIST, + NoSpecificBinaryOp.EQUAL_REAL, + NoSpecificBinaryOp.EQUAL_SET, + NoSpecificBinaryOp.EQUAL_STRING, + NoSpecificBinaryOp.EQUAL_TUPLE, + NoSpecificBinaryOp.GREATER_EQUAL_REALS, + NoSpecificBinaryOp.GREATER_THAN_REALS, + NoSpecificBinaryOp.INTEGER_DIVISION, + NoSpecificBinaryOp.LESS_EQUAL_REALS, + NoSpecificBinaryOp.LESS_THAN_REALS, + NoSpecificBinaryOp.MODULUS, + NoSpecificBinaryOp.MULTIPLICATION_REALS, + NoSpecificBinaryOp.SUBSET, + NoSpecificBinaryOp.SUBTRACTION_REALS, + NoSpecificBinaryOp.SUBTRACTION_LISTS, + NoSpecificBinaryOp.SUBTRACTION_SETS, + NoSpecificBinaryOp.SUBTRACTION_DICTS, + NoSpecificBinaryOp.UNEQUAL_DICT, + NoSpecificBinaryOp.UNEQUAL_LIST, + NoSpecificBinaryOp.UNEQUAL_REAL, + NoSpecificBinaryOp.UNEQUAL_SET, + NoSpecificBinaryOp.UNEQUAL_STRING, + NoSpecificBinaryOp.UNEQUAL_TUPLE), + new ExprNoSpecificUnaryExprsCheck( + NoSpecificUnaryOp.NEGATE_REALS, + NoSpecificUnaryOp.PLUS_REALS, + NoSpecificUnaryOp.SAMPLE) ); } -- GitLab From 0b22c861b95f9493dcc09f41003d4b1327c83efd Mon Sep 17 00:00:00 2001 From: Dennis Hendriks <dh_tue@hotmail.com> Date: Fri, 26 Jul 2024 12:38:55 +0200 Subject: [PATCH 14/20] #424 CIF to mCRL2 preconds move: no init preds in components. --- .../eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java | 4 ---- .../eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java | 6 +++++- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java index a52e396637..6a52690f1f 100644 --- a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java +++ b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java @@ -123,10 +123,6 @@ public class Cif2Mcrl2PreChecker { // IO declarations should be eliminated already. Assert.check(comp.getIoDecls().isEmpty()); - if (!comp.getInitials().isEmpty()) { - msg = fmt("Initialization predicates are not supported in %s.", CifTextUtils.getComponentText2(comp)); - problems.add(msg); - } if (!comp.getInvariants().isEmpty()) { msg = fmt("Invariants are not supported in %s.", CifTextUtils.getComponentText2(comp)); problems.add(msg); diff --git a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java index 2a962188c1..dd14bea078 100644 --- a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java +++ b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java @@ -15,6 +15,7 @@ package org.eclipse.escet.cif.cif2mcrl2; import org.eclipse.escet.cif.checkers.CifPreconditionChecker; import org.eclipse.escet.cif.checkers.checks.AutOnlyWithOneInitLocCheck; +import org.eclipse.escet.cif.checkers.checks.CompNoInitPredsCheck; import org.eclipse.escet.cif.checkers.checks.EdgeOnlySimpleAssignmentsCheck; import org.eclipse.escet.cif.checkers.checks.EqnNotAllowedCheck; import org.eclipse.escet.cif.checkers.checks.EventNoChannelsCheck; @@ -153,7 +154,10 @@ public class CifToMcrl2PreChecker extends CifPreconditionChecker { new ExprNoSpecificUnaryExprsCheck( NoSpecificUnaryOp.NEGATE_REALS, NoSpecificUnaryOp.PLUS_REALS, - NoSpecificUnaryOp.SAMPLE) + NoSpecificUnaryOp.SAMPLE), + + // No initialization predicates in components. + new CompNoInitPredsCheck() ); } -- GitLab From 66eb3a7bf68037554af2d92cf8f5d06fdd3189ce Mon Sep 17 00:00:00 2001 From: Dennis Hendriks <dh_tue@hotmail.com> Date: Fri, 26 Jul 2024 12:39:22 +0200 Subject: [PATCH 15/20] #424 CIF to mCRL2 preconds move: no invariants. --- .../cif/cif2mcrl2/Cif2Mcrl2PreChecker.java | 24 ------------------- .../cif/cif2mcrl2/CifToMcrl2PreChecker.java | 10 +++++++- 2 files changed, 9 insertions(+), 25 deletions(-) diff --git a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java index 6a52690f1f..73c8a9dccf 100644 --- a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java +++ b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java @@ -14,19 +14,15 @@ package org.eclipse.escet.cif.cif2mcrl2; import static org.eclipse.escet.common.java.Lists.list; -import static org.eclipse.escet.common.java.Strings.fmt; import java.util.Collections; import java.util.List; -import org.apache.commons.lang3.StringUtils; -import org.eclipse.escet.cif.common.CifTextUtils; import org.eclipse.escet.cif.metamodel.cif.ComplexComponent; import org.eclipse.escet.cif.metamodel.cif.Component; import org.eclipse.escet.cif.metamodel.cif.Group; 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.common.java.Assert; import org.eclipse.escet.common.java.Strings; import org.eclipse.escet.common.java.exceptions.InvalidInputException; @@ -96,20 +92,7 @@ public class Cif2Mcrl2PreChecker { * @param aut Automaton to check. */ private void checkAutomaton(Automaton aut) { - String msg; - checkComponent(aut); - - // Check locations. - for (Location loc: aut.getLocations()) { - String locTextMid = CifTextUtils.getLocationText2(loc); - String locTextStart = StringUtils.capitalize(locTextMid); - - if (!loc.getInvariants().isEmpty()) { - msg = locTextStart + " has invariants."; - problems.add(msg); - } - } } /** @@ -118,14 +101,7 @@ public class Cif2Mcrl2PreChecker { * @param comp Component to check. */ private void checkComponent(ComplexComponent comp) { - String msg; - // IO declarations should be eliminated already. Assert.check(comp.getIoDecls().isEmpty()); - - if (!comp.getInvariants().isEmpty()) { - msg = fmt("Invariants are not supported in %s.", CifTextUtils.getComponentText2(comp)); - problems.add(msg); - } } } diff --git a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java index dd14bea078..854674d7da 100644 --- a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java +++ b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java @@ -26,6 +26,7 @@ import org.eclipse.escet.cif.checkers.checks.ExprNoSpecificExprsCheck; import org.eclipse.escet.cif.checkers.checks.ExprNoSpecificExprsCheck.NoSpecificExpr; import org.eclipse.escet.cif.checkers.checks.ExprNoSpecificUnaryExprsCheck; import org.eclipse.escet.cif.checkers.checks.ExprNoSpecificUnaryExprsCheck.NoSpecificUnaryOp; +import org.eclipse.escet.cif.checkers.checks.InvNoSpecificInvsCheck; import org.eclipse.escet.cif.checkers.checks.SpecAutomataCountsCheck; import org.eclipse.escet.cif.checkers.checks.TypeNoSpecificTypesCheck; import org.eclipse.escet.cif.checkers.checks.TypeNoSpecificTypesCheck.NoSpecificType; @@ -33,6 +34,9 @@ import org.eclipse.escet.cif.checkers.checks.VarDiscOnlyStaticEvalInitCheck; import org.eclipse.escet.cif.checkers.checks.VarNoContinuousCheck; import org.eclipse.escet.cif.checkers.checks.VarNoDiscWithMultiInitValuesCheck; import org.eclipse.escet.cif.checkers.checks.VarNoInputCheck; +import org.eclipse.escet.cif.checkers.checks.invcheck.NoInvariantKind; +import org.eclipse.escet.cif.checkers.checks.invcheck.NoInvariantPlaceKind; +import org.eclipse.escet.cif.checkers.checks.invcheck.NoInvariantSupKind; import org.eclipse.escet.common.java.Termination; /** CIF to mCRL2 transformation precondition checker. */ @@ -157,7 +161,11 @@ public class CifToMcrl2PreChecker extends CifPreconditionChecker { NoSpecificUnaryOp.SAMPLE), // No initialization predicates in components. - new CompNoInitPredsCheck() + new CompNoInitPredsCheck(), + + // No invariants. + new InvNoSpecificInvsCheck().disallow( + NoInvariantSupKind.ALL_KINDS, NoInvariantKind.ALL_KINDS, NoInvariantPlaceKind.ALL_PLACES) ); } -- GitLab From f04fe1e98e0d9766db15b1c12231e7629cced0dd Mon Sep 17 00:00:00 2001 From: Dennis Hendriks <dh_tue@hotmail.com> Date: Fri, 26 Jul 2024 12:41:01 +0200 Subject: [PATCH 16/20] #424 Remove old CIF to mCRL2 precondition checker. --- .../cif/cif2mcrl2/Cif2Mcrl2PreChecker.java | 107 ------------------ 1 file changed, 107 deletions(-) delete mode 100644 cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java diff --git a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java deleted file mode 100644 index 73c8a9dccf..0000000000 --- a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java +++ /dev/null @@ -1,107 +0,0 @@ -////////////////////////////////////////////////////////////////////////////// -// Copyright (c) 2010, 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.cif2mcrl2; - -import static org.eclipse.escet.common.java.Lists.list; - -import java.util.Collections; -import java.util.List; - -import org.eclipse.escet.cif.metamodel.cif.ComplexComponent; -import org.eclipse.escet.cif.metamodel.cif.Component; -import org.eclipse.escet.cif.metamodel.cif.Group; -import org.eclipse.escet.cif.metamodel.cif.Specification; -import org.eclipse.escet.cif.metamodel.cif.automata.Automaton; -import org.eclipse.escet.common.java.Assert; -import org.eclipse.escet.common.java.Strings; -import org.eclipse.escet.common.java.exceptions.InvalidInputException; -import org.eclipse.escet.common.java.exceptions.UnsupportedException; - -/** Class for performing checks whether the specification can be used as input for the CIF to mCRL2 transformation. */ -public class Cif2Mcrl2PreChecker { - /** Found problems in the specification. */ - public List<String> problems = null; - - /** Constructor of the {@link Cif2Mcrl2PreChecker} class. */ - public Cif2Mcrl2PreChecker() { - // Nothing to do. - } - - /** - * Perform checks whether the specification is usable for performing a CIF to mCRL2 transformation. - * - * @param spec Specification to check. - * @throws InvalidInputException If the specification violates the pre-conditions. - */ - public void checkSpec(Specification spec) { - problems = list(); - checkGroup(spec); - - if (problems.isEmpty()) { - return; - } - // If we have any problems, the specification is unsupported. - Collections.sort(problems, Strings.SORTER); - if (!problems.isEmpty()) { - String msg = "CIF to mCRL2 transformation failed due to unsatisfied preconditions:\n - " - + String.join("\n - ", problems); - throw new UnsupportedException(msg); - } - } - - /** - * Unfold and check a group. - * - * @param grp Group to check and unfold. - */ - private void checkGroup(Group grp) { - // Definitions should be eliminated already. - Assert.check(grp.getDefinitions().isEmpty()); - checkComponent(grp); - - for (Component c: grp.getComponents()) { - if (c instanceof Automaton) { - Automaton aut = (Automaton)c; - checkAutomaton(aut); - continue; - } else if (c instanceof Group) { - Group g = (Group)c; - checkGroup(g); - continue; - } - - // ComponentInst should not happen, as DefInst has been eliminated. - throw new RuntimeException("Unexpected type of Component."); - } - } - - /** - * Check whether the automaton satisfies all pre-conditions of the CIF to mCRL2 transformation. - * - * @param aut Automaton to check. - */ - private void checkAutomaton(Automaton aut) { - checkComponent(aut); - } - - /** - * Verify that the given component does not have elements that are not supported in the translation. - * - * @param comp Component to check. - */ - private void checkComponent(ComplexComponent comp) { - // IO declarations should be eliminated already. - Assert.check(comp.getIoDecls().isEmpty()); - } -} -- GitLab From 4347eb3abdfd28f95f1aaae02d5b2d76413a3ff9 Mon Sep 17 00:00:00 2001 From: Dennis Hendriks <dh_tue@hotmail.com> Date: Fri, 26 Jul 2024 12:43:07 +0200 Subject: [PATCH 17/20] #424 Update rest of CIF to mCLR2 for removal of old precond checker. --- .../escet/cif/cif2mcrl2/storage/AutomatonData.java | 13 ------------- 1 file changed, 13 deletions(-) diff --git a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/storage/AutomatonData.java b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/storage/AutomatonData.java index d94692b7c8..4d860e611b 100644 --- a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/storage/AutomatonData.java +++ b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/storage/AutomatonData.java @@ -19,7 +19,6 @@ import static org.eclipse.escet.common.java.Sets.set; import java.util.Map; import java.util.Set; -import org.eclipse.escet.cif.cif2mcrl2.Cif2Mcrl2PreChecker; import org.eclipse.escet.cif.common.CifEventUtils; import org.eclipse.escet.cif.common.CifTextUtils; import org.eclipse.escet.cif.common.CifTypeUtils; @@ -75,10 +74,6 @@ public class AutomatonData { /** * Find discrete variables in an automaton. * - * <p> - * Copy of {@link Cif2Mcrl2PreChecker#checkAutomaton}, but without checking on acceptable constructs. - * </p> - * * @param variableMap Mapping of discrete variables in the meta model to their representation in the translation. */ public void addAutomatonVars(Map<DiscVariable, VariableData> variableMap) { @@ -162,10 +157,6 @@ public class AutomatonData { /** * Find discrete variables in an expression. * - * <p> - * Copy of {@link Cif2Mcrl2PreChecker#checkExpression}, but without checking on acceptable constructs. - * </p> - * * @param e Expression to inspect. * @return Used discrete variables in the expression. */ @@ -220,10 +211,6 @@ public class AutomatonData { /** * Get the events belonging to an edge. * - * <p> - * Copy of part of {@link Cif2Mcrl2PreChecker#checkAutomaton}, but without checking on allowed constructs. - * </p> - * * @param edge Edge to inspect. * @return The events of the edge. */ -- GitLab From 34e557df7a2620a66f55a8b16af0544cddf75ab3 Mon Sep 17 00:00:00 2001 From: Dennis Hendriks <dh_tue@hotmail.com> Date: Fri, 26 Jul 2024 12:45:05 +0200 Subject: [PATCH 18/20] #424 Adopt new CIF to mCRL2 precondition checker. --- .../eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2Application.java | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2Application.java b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2Application.java index 7dd967650f..287d6bb526 100644 --- a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2Application.java +++ b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2Application.java @@ -97,6 +97,7 @@ public class Cif2Mcrl2Application extends Application<IOutputComponent> { // Read CIF input. CifReader cifReader = new CifReader().init(); Specification spec = cifReader.read(); + String absSpecPath = Paths.resolve(InputFileOption.getPath()); if (isTerminationRequested()) { return 0; } @@ -123,9 +124,9 @@ public class Cif2Mcrl2Application extends Application<IOutputComponent> { return 0; } - // Check pre-conditions of the input. - Cif2Mcrl2PreChecker pca = new Cif2Mcrl2PreChecker(); - pca.checkSpec(spec); + // Check preconditions. + CifToMcrl2PreChecker checker = new CifToMcrl2PreChecker(() -> isTerminationRequested()); + checker.reportPreconditionViolations(spec, absSpecPath, "CIF to mCRL2 transformation"); if (isTerminationRequested()) { return 0; } -- GitLab From 3a167675c5ad724bb4ff9416ce064868ce2ba4ea Mon Sep 17 00:00:00 2001 From: Dennis Hendriks <dh_tue@hotmail.com> Date: Fri, 26 Jul 2024 12:56:18 +0200 Subject: [PATCH 19/20] #424 Update CIF to mCRL2 tests. --- .../tests/cif2mcrl2/invalid.cif | 26 +-- .../tests/cif2mcrl2/invalid.err | 167 ++++++++++++++++-- 2 files changed, 163 insertions(+), 30 deletions(-) diff --git a/cif/org.eclipse.escet.cif.tests/tests/cif2mcrl2/invalid.cif b/cif/org.eclipse.escet.cif.tests/tests/cif2mcrl2/invalid.cif index ec30f78b66..6961e85ffa 100644 --- a/cif/org.eclipse.escet.cif.tests/tests/cif2mcrl2/invalid.cif +++ b/cif/org.eclipse.escet.cif.tests/tests/cif2mcrl2/invalid.cif @@ -12,12 +12,12 @@ ////////////////////////////////////////////////////////////////////////////// group g: - event int[0..5] e1, e2; + event int[0..5] e1, e2; // Channels. - invariant 1 + 1 = 2; - invariant 1 = 3; // Non-true invariant in group. + invariant 1 + 1 = 2; // Invariant. + invariant 1 = 3; // Invariant. - initial 1 = 3; // Non-true initialization in group. + initial 1 = 3; // Initialization predicate in a component. automaton no_initial: // No initial location. location: @@ -35,24 +35,24 @@ group g: end plant p: - disc int[1..2] x1 in {1,2}; // Non-deterministic variable init. - disc int[1..2] x2 in any; // Non-deterministic variable init. + disc int[1..2] x1 in {1,2}; // Multiple potential initial values. + disc int[1..2] x2 in any; // Multiple potential initial values. cont cnt der 1.0; // Continuous variable, real type/value. disc list bool lb = [true]; // List type/expr. - plant invariant 1 + 1 = 2; - plant invariant 1 = 3; // Non-true invariant in automaton. + plant invariant 1 + 1 = 2; // Invariant. + plant invariant 1 = 3; // Invariant. location: initial true; edge e1 do if true: x1 := 2 end; // 'if' update. - edge e2 do lb := lb + [false]; + edge e2 do lb := lb + [false]; // List type/expr. - plant invariant 1+1 = 2; - plant invariant 1 = 3; // Non-true invariant in location. + plant invariant 1+1 = 2; // Invariant. + plant invariant 1 = 3; // Invariant. end - cont x der 1; - cont y; + cont x der 1; // Continuous variable. + cont y; // Continuous variable. equation y' = 2; // Equation. end diff --git a/cif/org.eclipse.escet.cif.tests/tests/cif2mcrl2/invalid.err b/cif/org.eclipse.escet.cif.tests/tests/cif2mcrl2/invalid.err index 37699c831f..455faaffa6 100644 --- a/cif/org.eclipse.escet.cif.tests/tests/cif2mcrl2/invalid.err +++ b/cif/org.eclipse.escet.cif.tests/tests/cif2mcrl2/invalid.err @@ -5,20 +5,153 @@ WARNING: File "cif2mcrl2/invalid.cif": Semantic warning at line 39, column 20: D WARNING: File "cif2mcrl2/invalid.cif": Semantic warning at line 43, column 11: Duplicate state invariant. WARNING: File "cif2mcrl2/invalid.cif": Semantic warning at line 44, column 11: Duplicate state invariant. ERROR: CIF to mCRL2 transformation failed due to unsatisfied preconditions: - - A value in the location of automaton "g.p" has an unsupported type "list bool" in expression "g.p.lb + [false]". - - Automaton "g.mult_initials" has more than one initial location. - - Automaton "g.no_initial" has no initial location. - - Continuous variable "g.p.cnt" is unsupported in the transformation. - - Continuous variable "g.x" is unsupported in the transformation. - - Continuous variable "g.y" is unsupported in the transformation. - - Discrete variable "g.p.lb" does not have a boolean, integer, or enumeration type. - - Discrete variable "g.p.x1" does not have a single initial value. - - Discrete variable "g.p.x2" does not have a single initial value. - - Equations are not supported in group "g". - - Initialization predicates are not supported in group "g". - - Invariants are not supported in automaton "g.p". - - Invariants are not supported in group "g". - - The location of automaton "g.no_initial" has a "tau" event. - - The location of automaton "g.no_initial" has a "tau" event. - - The location of automaton "g.p" has conditional updates. - - The location of automaton "g.p" has invariants. + + ------------------------------ + (1/16) A list literal is used. + ------------------------------ + * In automaton "g.p": + - edge e2 do lb := lb + [false]; + ^ + * In discrete variable "g.p.lb": + - disc list bool lb = [true]; + ^ + + --------------------------- + (2/16) A list type is used. + --------------------------- + * In automaton "g.p": + - edge e2 do lb := lb + [false]; + ^ ^ ^ ^ + * In discrete variable "g.p.lb": + - disc list bool lb = [true]; + ^ ^ + + ------------------------------------- + (3/16) A real number literal is used. + ------------------------------------- + * In group "g": + - equation y' = 2.0; + ^ + * In continuous variable "g.p.cnt": + - cont cnt = 0.0 der 1.0; + ^ ^ + * In continuous variable "g.x": + - cont x = 0.0 der 1.0; + ^ ^ + * In continuous variable "g.y": + - cont y = 0.0; + ^ + + --------------------------- + (4/16) A real type is used. + --------------------------- + * In group "g": + - equation y' = 2.0; + ^ + * In continuous variable "g.p.cnt": + - cont cnt = 0.0 der 1.0; + ^ ^ + * In continuous variable "g.x": + - cont x = 0.0 der 1.0; + ^ ^ + * In continuous variable "g.y": + - cont y = 0.0; + ^ + + --------------------------- + (5/16) An equation is used. + --------------------------- + * In group "g": + - equation y' = 2.0; + ^ + + ---------------------------- + (6/16) An invariant is used. + ---------------------------- + * In group "g": + - invariant false; + ^ + * In automaton "g.p": + - plant invariant false; + ^ + - plant invariant false; + ^ + + ------------------------------------------------ + (7/16) Automaton has multiple initial locations. + ------------------------------------------------ + * In group "g": + - automaton mult_initials: + ^ + + ----------------------------------------- + (8/16) Automaton has no initial location. + ----------------------------------------- + * In group "g": + - automaton no_initial: + ^ + + ----------------------------------------------------------- + (9/16) Binary operator "+" is used on a list typed operand. + ----------------------------------------------------------- + * In automaton "g.p": + - edge e2 do lb := lb + [false]; + ^ + + -------------------------------------------------- + (10/16) Component has an initialization predicate. + -------------------------------------------------- + * In group "g": + - initial false; + ^ + + ---------------------------------------------------------------- + (11/16) Discrete variable has multiple potential initial values. + ---------------------------------------------------------------- + * In automaton "g.p": + - disc int[1..2] x1 in {1, 2}; + ^ + + ------------------------------------------------------------------------------------------ + (12/16) Discrete variable has multiple potential initial values (any value in its domain). + ------------------------------------------------------------------------------------------ + * In automaton "g.p": + - disc int[1..2] x2 in any; + ^ + + -------------------------------- + (13/16) Edge has an 'if' update. + -------------------------------- + * In automaton "g.p": + - edge e1 do if true: x1 := 2 end; + ^ + + ----------------------------------------- + (14/16) Edge has an explicit 'tau' event. + ----------------------------------------- + * In automaton "g.no_initial": + - edge e1, e2, tau; + ^ + - edge tau; + ^ + + --------------------------- + (15/16) Event is a channel. + --------------------------- + * In group "g": + - event int[0..5] e1; + ^ + - event int[0..5] e2; + ^ + + ------------------------------------------ + (16/16) Variable is a continuous variable. + ------------------------------------------ + * In group "g": + - cont x = 0.0 der 1.0; + ^ + - cont y = 0.0; + ^ + * In automaton "g.p": + - cont cnt = 0.0 der 1.0; + ^ -- GitLab From 974a9c3dbf843e73873ab05a33352804d4bffed2 Mon Sep 17 00:00:00 2001 From: Dennis Hendriks <dh_tue@hotmail.com> Date: Fri, 26 Jul 2024 12:57:35 +0200 Subject: [PATCH 20/20] #424 Fix CIF to mCRL2 documentation. - Properly escape '=>'. - Binary operators '=' and '!=' are also supported for enums/ints. - Binary comparison operators are supported for ints. - Fixed English mistake. --- .../asciidoc/tools/cif2mcrl2.asciidoc | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/cif/org.eclipse.escet.cif.documentation/asciidoc/tools/cif2mcrl2.asciidoc b/cif/org.eclipse.escet.cif.documentation/asciidoc/tools/cif2mcrl2.asciidoc index 3922016b73..cfeee748a8 100644 --- a/cif/org.eclipse.escet.cif.documentation/asciidoc/tools/cif2mcrl2.asciidoc +++ b/cif/org.eclipse.escet.cif.documentation/asciidoc/tools/cif2mcrl2.asciidoc @@ -109,8 +109,10 @@ The latter may have a range. *** Boolean-typed constants are supported. *** Boolean-typed discrete variables are supported. *** Boolean-typed algebraic variables are supported. -*** Binary operators `and`, `or`, `==`, `!=` and `=>` on boolean-typed arguments are supported. -*** Unary operator `not` on boolean-typed arguments are supported. +*** Binary operators `and`, `or` and `+=>+` on boolean-typed arguments are supported. +*** Binary operators `=` and `!=` on boolean, enum and integer-typed arguments are supported. +*** Binary operators `<`, `+<=+`, `>` and `>=` on integer-typed arguments are supported. +*** Unary operator `not` on boolean-typed arguments is supported. *** Location references are not supported. ** Regarding enumeration-typed expressions (resulting in an enumeration literal as value): *** Enumeration literals are supported. -- GitLab