From 3ae730487ff3fe3d06f493be3845523940317741 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Bence=20T=C3=B3th?= Date: Thu, 20 Mar 2025 16:41:54 +0100 Subject: [PATCH 01/13] handle NotExpression --- .../ClockGuardTransformer.xtend | 64 +++++++++++++++++++ 1 file changed, 64 insertions(+) create mode 100644 plugins/xsts/hu.bme.mit.gamma.xsts.uppaal.transformation/src/hu/bme/mit/gamma/xsts/uppaal/transformation/ClockGuardTransformer.xtend diff --git a/plugins/xsts/hu.bme.mit.gamma.xsts.uppaal.transformation/src/hu/bme/mit/gamma/xsts/uppaal/transformation/ClockGuardTransformer.xtend b/plugins/xsts/hu.bme.mit.gamma.xsts.uppaal.transformation/src/hu/bme/mit/gamma/xsts/uppaal/transformation/ClockGuardTransformer.xtend new file mode 100644 index 000000000..94acd428b --- /dev/null +++ b/plugins/xsts/hu.bme.mit.gamma.xsts.uppaal.transformation/src/hu/bme/mit/gamma/xsts/uppaal/transformation/ClockGuardTransformer.xtend @@ -0,0 +1,64 @@ +package hu.bme.mit.gamma.xsts.uppaal.transformation + +import hu.bme.mit.gamma.expression.model.Expression +import java.util.List +import hu.bme.mit.gamma.expression.model.NotExpression +import hu.bme.mit.gamma.util.GammaEcoreUtil +import hu.bme.mit.gamma.expression.model.AndExpression +import hu.bme.mit.gamma.expression.model.ExpressionModelFactory +import hu.bme.mit.gamma.expression.model.OrExpression +import hu.bme.mit.gamma.expression.model.ReferenceExpression +import hu.bme.mit.gamma.expression.model.LiteralExpression +import hu.bme.mit.gamma.expression.model.PredicateExpression +import hu.bme.mit.gamma.expression.util.ExpressionNegator + +class ClockGuardTransformer { + protected final extension GammaEcoreUtil ecoreUtil = GammaEcoreUtil.INSTANCE + protected final extension ExpressionModelFactory constraintFactory = ExpressionModelFactory.eINSTANCE + protected final extension ExpressionNegator expressionNegator = ExpressionNegator.INSTANCE + + public static final ClockGuardTransformer INSTANCE = new ClockGuardTransformer + + def /*List*/ splitByDisjunction(Expression guard) { + try { + guard.toDnf + } catch (Exception e) { + } + } + + private dispatch def Expression toDnf(Expression exp) { + throw new IllegalArgumentException("Unhandled parameter types: " + exp); + } + + private dispatch def Expression toDnf(NotExpression expr) { + val innerExpr = expr.operand + if (innerExpr instanceof ReferenceExpression || innerExpr instanceof LiteralExpression || + innerExpr instanceof PredicateExpression) { + return expr + } + + // not not A => A + if (innerExpr instanceof NotExpression) { + return toDnf(innerExpr.operand) + } + // not (A and B) => (not A or not B) + if (innerExpr instanceof AndExpression) { + createOrExpression => [ + it.operands += innerExpr.operands.map [ + return toDnf(it.negate) + ] + ] + } + + // not (A or B) => (not A and not B) + if (innerExpr instanceof OrExpression) { + createAndExpression => [ + it.operands += innerExpr.operands.map [ + return toDnf(it.negate) + ] + ] + } + + throw new IllegalArgumentException("Unhandled parameter types: " + expr); + } +} From 405111fb8940ece24f784ae1ac9ad4ee9f96de71 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Bence=20T=C3=B3th?= Date: Thu, 20 Mar 2025 16:50:53 +0100 Subject: [PATCH 02/13] handle trivial expressions --- .../transformation/ClockGuardTransformer.xtend | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/plugins/xsts/hu.bme.mit.gamma.xsts.uppaal.transformation/src/hu/bme/mit/gamma/xsts/uppaal/transformation/ClockGuardTransformer.xtend b/plugins/xsts/hu.bme.mit.gamma.xsts.uppaal.transformation/src/hu/bme/mit/gamma/xsts/uppaal/transformation/ClockGuardTransformer.xtend index 94acd428b..e1593cf9b 100644 --- a/plugins/xsts/hu.bme.mit.gamma.xsts.uppaal.transformation/src/hu/bme/mit/gamma/xsts/uppaal/transformation/ClockGuardTransformer.xtend +++ b/plugins/xsts/hu.bme.mit.gamma.xsts.uppaal.transformation/src/hu/bme/mit/gamma/xsts/uppaal/transformation/ClockGuardTransformer.xtend @@ -29,9 +29,21 @@ class ClockGuardTransformer { private dispatch def Expression toDnf(Expression exp) { throw new IllegalArgumentException("Unhandled parameter types: " + exp); } + + private dispatch def Expression toDnf(ReferenceExpression exp){ + return exp + } + private dispatch def Expression toDnf(LiteralExpression exp){ + return exp + } + private dispatch def Expression toDnf(PredicateExpression exp){ + return exp + } private dispatch def Expression toDnf(NotExpression expr) { val innerExpr = expr.operand + + // A => A if (innerExpr instanceof ReferenceExpression || innerExpr instanceof LiteralExpression || innerExpr instanceof PredicateExpression) { return expr From 3d112e044fec824112e9cd2fa8ff0f508b2ec577 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Bence=20T=C3=B3th?= Date: Sat, 22 Mar 2025 16:08:07 +0100 Subject: [PATCH 03/13] handle AndExpressions --- .../ClockGuardTransformer.xtend | 90 ++++++++++++++++--- 1 file changed, 77 insertions(+), 13 deletions(-) diff --git a/plugins/xsts/hu.bme.mit.gamma.xsts.uppaal.transformation/src/hu/bme/mit/gamma/xsts/uppaal/transformation/ClockGuardTransformer.xtend b/plugins/xsts/hu.bme.mit.gamma.xsts.uppaal.transformation/src/hu/bme/mit/gamma/xsts/uppaal/transformation/ClockGuardTransformer.xtend index e1593cf9b..a2dd3e87b 100644 --- a/plugins/xsts/hu.bme.mit.gamma.xsts.uppaal.transformation/src/hu/bme/mit/gamma/xsts/uppaal/transformation/ClockGuardTransformer.xtend +++ b/plugins/xsts/hu.bme.mit.gamma.xsts.uppaal.transformation/src/hu/bme/mit/gamma/xsts/uppaal/transformation/ClockGuardTransformer.xtend @@ -21,7 +21,8 @@ class ClockGuardTransformer { def /*List*/ splitByDisjunction(Expression guard) { try { - guard.toDnf + val res = guard.clone.toDnf + true } catch (Exception e) { } } @@ -29,20 +30,22 @@ class ClockGuardTransformer { private dispatch def Expression toDnf(Expression exp) { throw new IllegalArgumentException("Unhandled parameter types: " + exp); } - - private dispatch def Expression toDnf(ReferenceExpression exp){ + + private dispatch def Expression toDnf(ReferenceExpression exp) { return exp - } - private dispatch def Expression toDnf(LiteralExpression exp){ + } + + private dispatch def Expression toDnf(LiteralExpression exp) { return exp - } - private dispatch def Expression toDnf(PredicateExpression exp){ + } + + private dispatch def Expression toDnf(PredicateExpression exp) { return exp - } + } private dispatch def Expression toDnf(NotExpression expr) { val innerExpr = expr.operand - + // A => A if (innerExpr instanceof ReferenceExpression || innerExpr instanceof LiteralExpression || innerExpr instanceof PredicateExpression) { @@ -55,22 +58,83 @@ class ClockGuardTransformer { } // not (A and B) => (not A or not B) if (innerExpr instanceof AndExpression) { - createOrExpression => [ + return createOrExpression => [ it.operands += innerExpr.operands.map [ - return toDnf(it.negate) + toDnf(it.negate) ] ] } // not (A or B) => (not A and not B) if (innerExpr instanceof OrExpression) { - createAndExpression => [ + return createAndExpression => [ it.operands += innerExpr.operands.map [ - return toDnf(it.negate) + toDnf(it.negate) ] ] } throw new IllegalArgumentException("Unhandled parameter types: " + expr); } + + private dispatch def Expression toDnf(AndExpression expr) { + val operands = expr.operands.map[toDnf] + + return distributeAnd(operands) + } + + /** + * This method may be used to distribute ANDs over ORs. + * + * @param operands list of operands + * + * @returns if distribution was necessary an `OrExpression`, otherwise an `AndExpression` + */ + private def Expression distributeAnd(List operands) { + if (!operands.exists[it instanceof OrExpression]) { + return createAndExpression => [ + it.operands += operands + ] + } + val listOfOperands = operands.map [ + if (it instanceof OrExpression) { + return it.operands + } + return #[it] + ] + val product = listProduct(listOfOperands).map [ ops | + createAndExpression => [ + it.operands += ops + ] + ] + + return createOrExpression => [ + it.operands += product + ] + } + + /** + * Creates a product of the inner lists + * + * @param list list of lists where each inner list must have at least 1 element + * + * @return every possible combination of the inner lists + */ + private def List> listProduct(List> list) { + if (list.empty) { + return #[] + } + if (list.length == 1) { + return list.head.map[#[it]] + } + val tails = listProduct(list.tail.clone) + // combine each current expression with each possible tail + return list.head.flatMap [ expr | + tails.map [ tail | + val product = newArrayList(expr.clone) + product += tail.clone + product + ] + ].clone + } } From eeb91f132812b7c248995ed75d5d0e6e428e4ba6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Bence=20T=C3=B3th?= Date: Sat, 22 Mar 2025 16:50:11 +0100 Subject: [PATCH 04/13] handle OrExpressions --- .../ClockGuardTransformer.xtend | 30 +++++++++++++++++-- 1 file changed, 27 insertions(+), 3 deletions(-) diff --git a/plugins/xsts/hu.bme.mit.gamma.xsts.uppaal.transformation/src/hu/bme/mit/gamma/xsts/uppaal/transformation/ClockGuardTransformer.xtend b/plugins/xsts/hu.bme.mit.gamma.xsts.uppaal.transformation/src/hu/bme/mit/gamma/xsts/uppaal/transformation/ClockGuardTransformer.xtend index a2dd3e87b..063117e51 100644 --- a/plugins/xsts/hu.bme.mit.gamma.xsts.uppaal.transformation/src/hu/bme/mit/gamma/xsts/uppaal/transformation/ClockGuardTransformer.xtend +++ b/plugins/xsts/hu.bme.mit.gamma.xsts.uppaal.transformation/src/hu/bme/mit/gamma/xsts/uppaal/transformation/ClockGuardTransformer.xtend @@ -11,18 +11,27 @@ import hu.bme.mit.gamma.expression.model.ReferenceExpression import hu.bme.mit.gamma.expression.model.LiteralExpression import hu.bme.mit.gamma.expression.model.PredicateExpression import hu.bme.mit.gamma.expression.util.ExpressionNegator +import hu.bme.mit.gamma.expression.util.ExpressionSerializer +import java.util.logging.Logger +import java.util.logging.Level class ClockGuardTransformer { protected final extension GammaEcoreUtil ecoreUtil = GammaEcoreUtil.INSTANCE protected final extension ExpressionModelFactory constraintFactory = ExpressionModelFactory.eINSTANCE protected final extension ExpressionNegator expressionNegator = ExpressionNegator.INSTANCE + + protected final extension ExpressionSerializer expressionSerializer=ExpressionSerializer.INSTANCE + protected final Logger logger = Logger.getLogger("GammaLogger") + public static final ClockGuardTransformer INSTANCE = new ClockGuardTransformer def /*List*/ splitByDisjunction(Expression guard) { try { - val res = guard.clone.toDnf - true + val clone=guard.clone + val preservedClone=guard.clone + val res = clone.toDnf + logger.log(Level.INFO, '''Before: «preservedClone.serialize»; After: «res.serialize»''') } catch (Exception e) { } } @@ -82,13 +91,28 @@ class ClockGuardTransformer { return distributeAnd(operands) } + + private dispatch def Expression toDnf(OrExpression expr){ + val operands=expr.operands.map[toDnf] + + val flattenedOperands=operands.flatMap[ + if(it instanceof OrExpression){ + return it.operands + } + return #[it] + ] + + return createOrExpression=>[ + it.operands+=flattenedOperands + ] + } /** * This method may be used to distribute ANDs over ORs. * * @param operands list of operands * - * @returns if distribution was necessary an `OrExpression`, otherwise an `AndExpression` + * @returns if distribution was necessary an `OrExpression`, otherwise an #[list.head]`AndExpression` */ private def Expression distributeAnd(List operands) { if (!operands.exists[it instanceof OrExpression]) { From 122663577604c7d4db6e831365f7c715f399a43b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Bence=20T=C3=B3th?= Date: Sat, 22 Mar 2025 18:57:17 +0100 Subject: [PATCH 05/13] integrate splitting into transformation, bugfixes using clone --- .../transformation/CfaActionTransformer.xtend | 53 ++++++++---- .../ClockGuardTransformer.xtend | 84 ++++++++----------- .../XstsToUppaalTransformer.xtend | 58 +++++++------ 3 files changed, 103 insertions(+), 92 deletions(-) diff --git a/plugins/xsts/hu.bme.mit.gamma.xsts.uppaal.transformation/src/hu/bme/mit/gamma/xsts/uppaal/transformation/CfaActionTransformer.xtend b/plugins/xsts/hu.bme.mit.gamma.xsts.uppaal.transformation/src/hu/bme/mit/gamma/xsts/uppaal/transformation/CfaActionTransformer.xtend index 5d8fc8592..6351d52ef 100644 --- a/plugins/xsts/hu.bme.mit.gamma.xsts.uppaal.transformation/src/hu/bme/mit/gamma/xsts/uppaal/transformation/CfaActionTransformer.xtend +++ b/plugins/xsts/hu.bme.mit.gamma.xsts.uppaal.transformation/src/hu/bme/mit/gamma/xsts/uppaal/transformation/CfaActionTransformer.xtend @@ -53,6 +53,8 @@ class CfaActionTransformer { protected final extension ExpressionEvaluator evaluator = ExpressionEvaluator.INSTANCE protected final extension GammaEcoreUtil ecoreUtil = GammaEcoreUtil.INSTANCE + protected final extension ClockGuardTransformer clockGuardTransformer = ClockGuardTransformer.INSTANCE + new(NtaBuilder ntaBuilder, Traceability traceability) { this.ntaBuilder = ntaBuilder this.traceability = traceability @@ -143,11 +145,18 @@ class CfaActionTransformer { } protected def dispatch Location transformAction(AssumeAction action, Location source) { - val edge = source.createEdgeCommittedSource(nextCommittedLocationName) - val uppaalExpression = action.assumption.transform - edge.guard = uppaalExpression - - return edge.target + val target = createLocation(source.parentTemplate) => [ + it.name = nextCommittedLocationName + it.locationTimeKind = LocationKind.COMMITED + ] + val guards = action.assumption.splitByDisjunction.map[transform] + for (guard : guards) { + source.createEdge(target) => [ + it.guard = guard + ] + } + + return target } protected def dispatch Location transformAction(SequentialAction action, Location source) { @@ -187,23 +196,37 @@ class CfaActionTransformer { val condition = action.condition - val positiveCondition = condition.transform + val positiveCondition = condition val negativeCondition = condition.clone - .createNotExpression.transform + .createNotExpression - val thenEdge = source.createEdgeCommittedSource(nextCommittedLocationName) - thenEdge.guard = positiveCondition - val thenEdgeTarget = thenEdge.target + val thenGuardTarget = createLocation(source.parentTemplate) => [ + it.name = nextCommittedLocationName + it.locationTimeKind = LocationKind.COMMITED + ] + val thenGuards = positiveCondition.splitByDisjunction.map[transform] + for (guard : thenGuards) { + source.createEdge(thenGuardTarget) => [ + it.guard = guard + ] + } val thenAction = action.then - val thenActionTarget = thenAction.transformAction(thenEdgeTarget) + val thenActionTarget = thenAction.transformAction(thenGuardTarget) - val elseEdge = source.createEdgeCommittedSource(nextCommittedLocationName) - elseEdge.guard = negativeCondition - val elseEdgeTarget = elseEdge.target + val elseGuardTarget = createLocation(source.parentTemplate) => [ + it.name = nextCommittedLocationName + it.locationTimeKind = LocationKind.COMMITED + ] + val elseGuards = negativeCondition.splitByDisjunction.map[transform] + for (guard : elseGuards) { + source.createEdge(elseGuardTarget) => [ + it.guard = guard + ] + } val elseAction = action.^else - val elseActionTarget = (elseAction !== null) ? elseAction.transformAction(elseEdgeTarget) : elseEdgeTarget + val elseActionTarget = (elseAction !== null) ? elseAction.transformAction(elseGuardTarget) : elseGuardTarget elseActionTarget.createEdge(thenActionTarget) diff --git a/plugins/xsts/hu.bme.mit.gamma.xsts.uppaal.transformation/src/hu/bme/mit/gamma/xsts/uppaal/transformation/ClockGuardTransformer.xtend b/plugins/xsts/hu.bme.mit.gamma.xsts.uppaal.transformation/src/hu/bme/mit/gamma/xsts/uppaal/transformation/ClockGuardTransformer.xtend index 063117e51..ad1be8f55 100644 --- a/plugins/xsts/hu.bme.mit.gamma.xsts.uppaal.transformation/src/hu/bme/mit/gamma/xsts/uppaal/transformation/ClockGuardTransformer.xtend +++ b/plugins/xsts/hu.bme.mit.gamma.xsts.uppaal.transformation/src/hu/bme/mit/gamma/xsts/uppaal/transformation/ClockGuardTransformer.xtend @@ -19,21 +19,25 @@ class ClockGuardTransformer { protected final extension GammaEcoreUtil ecoreUtil = GammaEcoreUtil.INSTANCE protected final extension ExpressionModelFactory constraintFactory = ExpressionModelFactory.eINSTANCE protected final extension ExpressionNegator expressionNegator = ExpressionNegator.INSTANCE - - protected final extension ExpressionSerializer expressionSerializer=ExpressionSerializer.INSTANCE - protected final Logger logger = Logger.getLogger("GammaLogger") - + + protected final extension ExpressionSerializer expressionSerializer = ExpressionSerializer.INSTANCE + protected final Logger logger = Logger.getLogger("GammaLogger") public static final ClockGuardTransformer INSTANCE = new ClockGuardTransformer - def /*List*/ splitByDisjunction(Expression guard) { - try { - val clone=guard.clone - val preservedClone=guard.clone - val res = clone.toDnf - logger.log(Level.INFO, '''Before: «preservedClone.serialize»; After: «res.serialize»''') - } catch (Exception e) { + def List splitByDisjunction(Expression guard) { + val clone = guard.clone + val preservedClone = guard.clone + if (preservedClone.serialize == + "!((((main_region_of_bJbCOID_allapotgep_coid == Main_region_of_bJbCOID_allapotgep_bJbCOID_allapotgep::Oldas_4) && ((I_CR_h_In_hValue_coid != MyBool::_1) || (I_FT_h_In_hValue_coid != MyBool::_1))) || ((main_region_of_bJbCOID_allapotgep_coid == Main_region_of_bJbCOID_allapotgep_bJbCOID_allapotgep::Celoldas_idozites_nem_fut_5) && (I_CR_h_In_hValue_coid == MyBool::_1) && (I_FT_h_In_hValue_coid == MyBool::_1)) || ((main_region_of_bJbCOID_allapotgep_coid == Main_region_of_bJbCOID_allapotgep_bJbCOID_allapotgep::Celoldas_idozites_fut_8) && (499 <= P_COIDH_Timeout_coid) && (I_CR_h_In_hValue_coid == MyBool::_1) && (I_FT_h_In_hValue_coid == MyBool::_1)) || ((main_region_of_bJbCOID_allapotgep_coid == Main_region_of_bJbCOID_allapotgep_bJbCOID_allapotgep::Celoldas_idozites_fut_8) && ((I_CR_h_In_hValue_coid != MyBool::_1) || (I_FT_h_In_hValue_coid != MyBool::_1)))))") { + logger.log(Level.INFO, "foo") + } + val transformed = clone.toDnf + logger.log(Level.INFO, '''Before: «preservedClone.serialize»; After: «transformed.serialize»''') + if (transformed instanceof OrExpression) { + return transformed.operands } + return #[transformed] } private dispatch def Expression toDnf(Expression exp) { @@ -41,49 +45,27 @@ class ClockGuardTransformer { } private dispatch def Expression toDnf(ReferenceExpression exp) { - return exp + return exp.clone } private dispatch def Expression toDnf(LiteralExpression exp) { - return exp + return exp.clone } private dispatch def Expression toDnf(PredicateExpression exp) { - return exp + return exp.clone } private dispatch def Expression toDnf(NotExpression expr) { val innerExpr = expr.operand - // A => A - if (innerExpr instanceof ReferenceExpression || innerExpr instanceof LiteralExpression || - innerExpr instanceof PredicateExpression) { - return expr + // not A => not A + // necessary to avoid infinite recursion + if (innerExpr instanceof ReferenceExpression) { + return expr.clone } - - // not not A => A - if (innerExpr instanceof NotExpression) { - return toDnf(innerExpr.operand) - } - // not (A and B) => (not A or not B) - if (innerExpr instanceof AndExpression) { - return createOrExpression => [ - it.operands += innerExpr.operands.map [ - toDnf(it.negate) - ] - ] - } - - // not (A or B) => (not A and not B) - if (innerExpr instanceof OrExpression) { - return createAndExpression => [ - it.operands += innerExpr.operands.map [ - toDnf(it.negate) - ] - ] - } - - throw new IllegalArgumentException("Unhandled parameter types: " + expr); + // handles DeMorgan transformations + return innerExpr.negate.toDnf } private dispatch def Expression toDnf(AndExpression expr) { @@ -91,19 +73,19 @@ class ClockGuardTransformer { return distributeAnd(operands) } - - private dispatch def Expression toDnf(OrExpression expr){ - val operands=expr.operands.map[toDnf] - - val flattenedOperands=operands.flatMap[ - if(it instanceof OrExpression){ + + private dispatch def Expression toDnf(OrExpression expr) { + val operands = expr.operands.map[toDnf] + + val flattenedOperands = operands.flatMap [ + if (it instanceof OrExpression) { return it.operands } return #[it] ] - - return createOrExpression=>[ - it.operands+=flattenedOperands + + return createOrExpression => [ + it.operands += flattenedOperands.clone ] } diff --git a/plugins/xsts/hu.bme.mit.gamma.xsts.uppaal.transformation/src/hu/bme/mit/gamma/xsts/uppaal/transformation/XstsToUppaalTransformer.xtend b/plugins/xsts/hu.bme.mit.gamma.xsts.uppaal.transformation/src/hu/bme/mit/gamma/xsts/uppaal/transformation/XstsToUppaalTransformer.xtend index f53bf5fd1..dcea5043f 100644 --- a/plugins/xsts/hu.bme.mit.gamma.xsts.uppaal.transformation/src/hu/bme/mit/gamma/xsts/uppaal/transformation/XstsToUppaalTransformer.xtend +++ b/plugins/xsts/hu.bme.mit.gamma.xsts.uppaal.transformation/src/hu/bme/mit/gamma/xsts/uppaal/transformation/XstsToUppaalTransformer.xtend @@ -1,11 +1,11 @@ /******************************************************************************** * Copyright (c) 2018-2023 Contributors to the Gamma project - * + * * All rights reserved. This program and the accompanying materials * are made available under the terms of the Eclipse Public License v1.0 * which accompanies this distribution, and is available at * http://www.eclipse.org/legal/epl-v10.html - * + * * SPDX-License-Identifier: EPL-1.0 ********************************************************************************/ package hu.bme.mit.gamma.xsts.uppaal.transformation @@ -26,22 +26,22 @@ import static hu.bme.mit.gamma.uppaal.util.XstsNamings.* import static extension hu.bme.mit.gamma.xsts.derivedfeatures.XstsDerivedFeatures.* class XstsToUppaalTransformer { - + protected final XSTS xSts protected final Traceability traceability - + // Auxiliary protected final extension NtaBuilder ntaBuilder protected final extension CfaActionTransformer actionTransformer protected final extension FunctionActionTransformer functionctionTransformer protected final extension VariableTransformer variableTransformer protected final extension NtaOptimizer ntaOptimizer - + protected final extension GammaEcoreUtil ecoreUtil = GammaEcoreUtil.INSTANCE protected final extension ClockExpressionHandler clockExpressionHandler = ClockExpressionHandler.INSTANCE - + protected final Logger logger = Logger.getLogger("GammaLogger") - + new(XSTS xSts) { this.xSts = xSts this.ntaBuilder = new NtaBuilder(xSts.name, false) @@ -51,63 +51,69 @@ class XstsToUppaalTransformer { this.variableTransformer = new VariableTransformer(ntaBuilder, traceability) this.ntaOptimizer = new NtaOptimizer(ntaBuilder) } - + def execute() { // If the XSTS transformation extracts guards into local variables: // if the guard contains clock variables (referencing native clocks), they should be reinlined - resetCommittedLocationName val initialLocation = templateName.createTemplateWithInitLoc(initialLocationName) initialLocation.locationTimeKind = LocationKind.COMMITED val template = initialLocation.parentTemplate - + val initializingAction = xSts.initializingAction val environmentalAction = xSts.environmentalAction val mergedAction = xSts.mergedAction - + xSts.transformVariables - + val stableLocation = initializingAction.transformAction(initialLocation) stableLocation.name = stableLocationName stableLocation.locationTimeKind = LocationKind.NORMAL - + val environmentFinishLocation = template.createLocation environmentFinishLocation.name = environmentFinishLocationName // Location kind is Normal, so optimization does not delete it environmentalAction.transformIntoCfa(stableLocation, environmentFinishLocation) - - if (mergedAction.isOrContainsTypes(#[NonDeterministicAction, HavocAction]) || - xSts.hasClockVariable || xSts.hasInvariants) { + + if (mergedAction.isOrContainsTypes(#[NonDeterministicAction, HavocAction]) || xSts.hasClockVariable || + xSts.hasInvariants) { // For nondeterministic cases, UPPAAL functions cannot be used mergedAction.transformIntoCfa(environmentFinishLocation, stableLocation) - } - else { + } else { // Deterministic behavior, creating a function mergedAction.transformIntoFunction(environmentFinishLocation, stableLocation) } - + // Optimizing edges from these location + val before=ntaBuilder.nta.template.head.location.length initialLocation.optimizeSubsequentEdges + val afterInit=ntaBuilder.nta.template.head.location.length stableLocation.optimizeSubsequentEdges + val afterStable=ntaBuilder.nta.template.head.location.length environmentFinishLocation.optimizeSubsequentEdges + val afterEnv=ntaBuilder.nta.template.head.location.length + if(afterInit!=afterStable||afterStable!=afterEnv){ + logger.log(Level.INFO, "hmmmm") + } + if (environmentFinishLocation !== stableLocation) { // Model checking is faster if the environment finish location is committed environmentFinishLocation.locationTimeKind = LocationKind.COMMITED } - + logger.log(Level.INFO, "Basic NTA transformation has finished") - + // optimizelIntegerCodomains // val nta = ntaBuilder.nta - nta.transformClockExpressions + //done during transforIntoCfa + //nta.transformClockExpressions // - ntaBuilder.instantiateTemplates - + return nta } - -} \ No newline at end of file + +} From 7914883c6da0c97e374c5366c4ffc4e9d9e2d40a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Bence=20T=C3=B3th?= Date: Sat, 22 Mar 2025 19:14:26 +0100 Subject: [PATCH 06/13] remove debug statements --- .../ClockGuardTransformer.xtend | 4 -- .../XstsToUppaalTransformer.xtend | 58 +++++++++---------- 2 files changed, 26 insertions(+), 36 deletions(-) diff --git a/plugins/xsts/hu.bme.mit.gamma.xsts.uppaal.transformation/src/hu/bme/mit/gamma/xsts/uppaal/transformation/ClockGuardTransformer.xtend b/plugins/xsts/hu.bme.mit.gamma.xsts.uppaal.transformation/src/hu/bme/mit/gamma/xsts/uppaal/transformation/ClockGuardTransformer.xtend index ad1be8f55..baaea2850 100644 --- a/plugins/xsts/hu.bme.mit.gamma.xsts.uppaal.transformation/src/hu/bme/mit/gamma/xsts/uppaal/transformation/ClockGuardTransformer.xtend +++ b/plugins/xsts/hu.bme.mit.gamma.xsts.uppaal.transformation/src/hu/bme/mit/gamma/xsts/uppaal/transformation/ClockGuardTransformer.xtend @@ -28,10 +28,6 @@ class ClockGuardTransformer { def List splitByDisjunction(Expression guard) { val clone = guard.clone val preservedClone = guard.clone - if (preservedClone.serialize == - "!((((main_region_of_bJbCOID_allapotgep_coid == Main_region_of_bJbCOID_allapotgep_bJbCOID_allapotgep::Oldas_4) && ((I_CR_h_In_hValue_coid != MyBool::_1) || (I_FT_h_In_hValue_coid != MyBool::_1))) || ((main_region_of_bJbCOID_allapotgep_coid == Main_region_of_bJbCOID_allapotgep_bJbCOID_allapotgep::Celoldas_idozites_nem_fut_5) && (I_CR_h_In_hValue_coid == MyBool::_1) && (I_FT_h_In_hValue_coid == MyBool::_1)) || ((main_region_of_bJbCOID_allapotgep_coid == Main_region_of_bJbCOID_allapotgep_bJbCOID_allapotgep::Celoldas_idozites_fut_8) && (499 <= P_COIDH_Timeout_coid) && (I_CR_h_In_hValue_coid == MyBool::_1) && (I_FT_h_In_hValue_coid == MyBool::_1)) || ((main_region_of_bJbCOID_allapotgep_coid == Main_region_of_bJbCOID_allapotgep_bJbCOID_allapotgep::Celoldas_idozites_fut_8) && ((I_CR_h_In_hValue_coid != MyBool::_1) || (I_FT_h_In_hValue_coid != MyBool::_1)))))") { - logger.log(Level.INFO, "foo") - } val transformed = clone.toDnf logger.log(Level.INFO, '''Before: «preservedClone.serialize»; After: «transformed.serialize»''') if (transformed instanceof OrExpression) { diff --git a/plugins/xsts/hu.bme.mit.gamma.xsts.uppaal.transformation/src/hu/bme/mit/gamma/xsts/uppaal/transformation/XstsToUppaalTransformer.xtend b/plugins/xsts/hu.bme.mit.gamma.xsts.uppaal.transformation/src/hu/bme/mit/gamma/xsts/uppaal/transformation/XstsToUppaalTransformer.xtend index dcea5043f..aa4527355 100644 --- a/plugins/xsts/hu.bme.mit.gamma.xsts.uppaal.transformation/src/hu/bme/mit/gamma/xsts/uppaal/transformation/XstsToUppaalTransformer.xtend +++ b/plugins/xsts/hu.bme.mit.gamma.xsts.uppaal.transformation/src/hu/bme/mit/gamma/xsts/uppaal/transformation/XstsToUppaalTransformer.xtend @@ -1,11 +1,11 @@ /******************************************************************************** * Copyright (c) 2018-2023 Contributors to the Gamma project - * + * * All rights reserved. This program and the accompanying materials * are made available under the terms of the Eclipse Public License v1.0 * which accompanies this distribution, and is available at * http://www.eclipse.org/legal/epl-v10.html - * + * * SPDX-License-Identifier: EPL-1.0 ********************************************************************************/ package hu.bme.mit.gamma.xsts.uppaal.transformation @@ -26,22 +26,22 @@ import static hu.bme.mit.gamma.uppaal.util.XstsNamings.* import static extension hu.bme.mit.gamma.xsts.derivedfeatures.XstsDerivedFeatures.* class XstsToUppaalTransformer { - + protected final XSTS xSts protected final Traceability traceability - + // Auxiliary protected final extension NtaBuilder ntaBuilder protected final extension CfaActionTransformer actionTransformer protected final extension FunctionActionTransformer functionctionTransformer protected final extension VariableTransformer variableTransformer protected final extension NtaOptimizer ntaOptimizer - + protected final extension GammaEcoreUtil ecoreUtil = GammaEcoreUtil.INSTANCE protected final extension ClockExpressionHandler clockExpressionHandler = ClockExpressionHandler.INSTANCE - + protected final Logger logger = Logger.getLogger("GammaLogger") - + new(XSTS xSts) { this.xSts = xSts this.ntaBuilder = new NtaBuilder(xSts.name, false) @@ -51,69 +51,63 @@ class XstsToUppaalTransformer { this.variableTransformer = new VariableTransformer(ntaBuilder, traceability) this.ntaOptimizer = new NtaOptimizer(ntaBuilder) } - + def execute() { // If the XSTS transformation extracts guards into local variables: // if the guard contains clock variables (referencing native clocks), they should be reinlined + resetCommittedLocationName val initialLocation = templateName.createTemplateWithInitLoc(initialLocationName) initialLocation.locationTimeKind = LocationKind.COMMITED val template = initialLocation.parentTemplate - + val initializingAction = xSts.initializingAction val environmentalAction = xSts.environmentalAction val mergedAction = xSts.mergedAction - + xSts.transformVariables - + val stableLocation = initializingAction.transformAction(initialLocation) stableLocation.name = stableLocationName stableLocation.locationTimeKind = LocationKind.NORMAL - + val environmentFinishLocation = template.createLocation environmentFinishLocation.name = environmentFinishLocationName // Location kind is Normal, so optimization does not delete it environmentalAction.transformIntoCfa(stableLocation, environmentFinishLocation) - - if (mergedAction.isOrContainsTypes(#[NonDeterministicAction, HavocAction]) || xSts.hasClockVariable || - xSts.hasInvariants) { + + if (mergedAction.isOrContainsTypes(#[NonDeterministicAction, HavocAction]) || + xSts.hasClockVariable || xSts.hasInvariants) { // For nondeterministic cases, UPPAAL functions cannot be used mergedAction.transformIntoCfa(environmentFinishLocation, stableLocation) - } else { + } + else { // Deterministic behavior, creating a function mergedAction.transformIntoFunction(environmentFinishLocation, stableLocation) } - + // Optimizing edges from these location - val before=ntaBuilder.nta.template.head.location.length initialLocation.optimizeSubsequentEdges - val afterInit=ntaBuilder.nta.template.head.location.length stableLocation.optimizeSubsequentEdges - val afterStable=ntaBuilder.nta.template.head.location.length environmentFinishLocation.optimizeSubsequentEdges - val afterEnv=ntaBuilder.nta.template.head.location.length - if(afterInit!=afterStable||afterStable!=afterEnv){ - logger.log(Level.INFO, "hmmmm") - } - if (environmentFinishLocation !== stableLocation) { // Model checking is faster if the environment finish location is committed environmentFinishLocation.locationTimeKind = LocationKind.COMMITED } - + logger.log(Level.INFO, "Basic NTA transformation has finished") - + // optimizelIntegerCodomains // val nta = ntaBuilder.nta - //done during transforIntoCfa - //nta.transformClockExpressions + //nta.transformClockExpressions CFA transformer handles it // + ntaBuilder.instantiateTemplates - + return nta } - -} + +} \ No newline at end of file From 1ee0dbd847c5eed0376c62323f9e73ca79a13da7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Bence=20T=C3=B3th?= Date: Sun, 23 Mar 2025 17:48:46 +0100 Subject: [PATCH 07/13] only transform if subtree contains clock reference --- .../ClockGuardTransformer.xtend | 36 ++++++++++++++++--- 1 file changed, 31 insertions(+), 5 deletions(-) diff --git a/plugins/xsts/hu.bme.mit.gamma.xsts.uppaal.transformation/src/hu/bme/mit/gamma/xsts/uppaal/transformation/ClockGuardTransformer.xtend b/plugins/xsts/hu.bme.mit.gamma.xsts.uppaal.transformation/src/hu/bme/mit/gamma/xsts/uppaal/transformation/ClockGuardTransformer.xtend index baaea2850..4798f4cff 100644 --- a/plugins/xsts/hu.bme.mit.gamma.xsts.uppaal.transformation/src/hu/bme/mit/gamma/xsts/uppaal/transformation/ClockGuardTransformer.xtend +++ b/plugins/xsts/hu.bme.mit.gamma.xsts.uppaal.transformation/src/hu/bme/mit/gamma/xsts/uppaal/transformation/ClockGuardTransformer.xtend @@ -14,11 +14,16 @@ import hu.bme.mit.gamma.expression.util.ExpressionNegator import hu.bme.mit.gamma.expression.util.ExpressionSerializer import java.util.logging.Logger import java.util.logging.Level +import hu.bme.mit.gamma.expression.util.ExpressionEvaluator +import hu.bme.mit.gamma.expression.model.DirectReferenceExpression +import hu.bme.mit.gamma.expression.model.VariableDeclaration +import hu.bme.mit.gamma.expression.model.ClockVariableDeclarationAnnotation class ClockGuardTransformer { protected final extension GammaEcoreUtil ecoreUtil = GammaEcoreUtil.INSTANCE protected final extension ExpressionModelFactory constraintFactory = ExpressionModelFactory.eINSTANCE protected final extension ExpressionNegator expressionNegator = ExpressionNegator.INSTANCE + protected final extension ExpressionEvaluator expressionEvaluator = ExpressionEvaluator.INSTANCE protected final extension ExpressionSerializer expressionSerializer = ExpressionSerializer.INSTANCE protected final Logger logger = Logger.getLogger("GammaLogger") @@ -28,14 +33,21 @@ class ClockGuardTransformer { def List splitByDisjunction(Expression guard) { val clone = guard.clone val preservedClone = guard.clone - val transformed = clone.toDnf + val transformed = clone.toDnfChecked logger.log(Level.INFO, '''Before: «preservedClone.serialize»; After: «transformed.serialize»''') if (transformed instanceof OrExpression) { - return transformed.operands + return transformed.operands.reject[it.isDefinitelyFalseExpression].clone } return #[transformed] } + private def Expression toDnfChecked(Expression exp) { + if (exp.containsClockReference) { + return toDnf(exp) + } + return exp.clone + } + private dispatch def Expression toDnf(Expression exp) { throw new IllegalArgumentException("Unhandled parameter types: " + exp); } @@ -61,17 +73,17 @@ class ClockGuardTransformer { return expr.clone } // handles DeMorgan transformations - return innerExpr.negate.toDnf + return innerExpr.negate.toDnfChecked } private dispatch def Expression toDnf(AndExpression expr) { - val operands = expr.operands.map[toDnf] + val operands = expr.operands.map[toDnfChecked] return distributeAnd(operands) } private dispatch def Expression toDnf(OrExpression expr) { - val operands = expr.operands.map[toDnf] + val operands = expr.operands.map[toDnfChecked] val flattenedOperands = operands.flatMap [ if (it instanceof OrExpression) { @@ -139,4 +151,18 @@ class ClockGuardTransformer { ] ].clone } + + private def containsClockReference(Expression expression) { + return expression !== null && expression.getSelfAndAllContentsOfType(DirectReferenceExpression).exists [ + it.clock + ] + } + + private def boolean isClock(DirectReferenceExpression expr) { + val declaration = expr.declaration + if (declaration instanceof VariableDeclaration) { + return declaration.annotations.exists[it instanceof ClockVariableDeclarationAnnotation] + } + return false + } } From debc446ddfdb6ea10550183c0de59b6ded9f9f03 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Bence=20T=C3=B3th?= Date: Wed, 2 Apr 2025 19:49:11 +0200 Subject: [PATCH 08/13] Add extra comment --- .../xsts/uppaal/transformation/XstsToUppaalTransformer.xtend | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/plugins/xsts/hu.bme.mit.gamma.xsts.uppaal.transformation/src/hu/bme/mit/gamma/xsts/uppaal/transformation/XstsToUppaalTransformer.xtend b/plugins/xsts/hu.bme.mit.gamma.xsts.uppaal.transformation/src/hu/bme/mit/gamma/xsts/uppaal/transformation/XstsToUppaalTransformer.xtend index aa4527355..c296703cf 100644 --- a/plugins/xsts/hu.bme.mit.gamma.xsts.uppaal.transformation/src/hu/bme/mit/gamma/xsts/uppaal/transformation/XstsToUppaalTransformer.xtend +++ b/plugins/xsts/hu.bme.mit.gamma.xsts.uppaal.transformation/src/hu/bme/mit/gamma/xsts/uppaal/transformation/XstsToUppaalTransformer.xtend @@ -102,7 +102,7 @@ class XstsToUppaalTransformer { optimizelIntegerCodomains // val nta = ntaBuilder.nta - //nta.transformClockExpressions CFA transformer handles it + //nta.transformClockExpressions // CFA transformer handles it // ntaBuilder.instantiateTemplates From 0a366da40dc37ed1816313c96dd53a2d94d782a0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Bence=20T=C3=B3th?= Date: Wed, 2 Apr 2025 20:34:40 +0200 Subject: [PATCH 09/13] documentation --- .../ClockGuardTransformer.xtend | 44 ++++++++++++++++--- 1 file changed, 39 insertions(+), 5 deletions(-) diff --git a/plugins/xsts/hu.bme.mit.gamma.xsts.uppaal.transformation/src/hu/bme/mit/gamma/xsts/uppaal/transformation/ClockGuardTransformer.xtend b/plugins/xsts/hu.bme.mit.gamma.xsts.uppaal.transformation/src/hu/bme/mit/gamma/xsts/uppaal/transformation/ClockGuardTransformer.xtend index 4798f4cff..4e82a05ed 100644 --- a/plugins/xsts/hu.bme.mit.gamma.xsts.uppaal.transformation/src/hu/bme/mit/gamma/xsts/uppaal/transformation/ClockGuardTransformer.xtend +++ b/plugins/xsts/hu.bme.mit.gamma.xsts.uppaal.transformation/src/hu/bme/mit/gamma/xsts/uppaal/transformation/ClockGuardTransformer.xtend @@ -19,6 +19,14 @@ import hu.bme.mit.gamma.expression.model.DirectReferenceExpression import hu.bme.mit.gamma.expression.model.VariableDeclaration import hu.bme.mit.gamma.expression.model.ClockVariableDeclarationAnnotation + +/** + * A utility class that brings guard expressions to DNF form in regard to clock variables. + * + * UPPAAL requires, that 'A guard must be a conjunction of simple conditions on clocks, + * differences between clocks, and boolean expressions not involving clocks.' + * This class can bring an expression to DNF form so it may be split across edges. + */ class ClockGuardTransformer { protected final extension GammaEcoreUtil ecoreUtil = GammaEcoreUtil.INSTANCE protected final extension ExpressionModelFactory constraintFactory = ExpressionModelFactory.eINSTANCE @@ -28,19 +36,33 @@ class ClockGuardTransformer { protected final extension ExpressionSerializer expressionSerializer = ExpressionSerializer.INSTANCE protected final Logger logger = Logger.getLogger("GammaLogger") + /// Singleton class instance public static final ClockGuardTransformer INSTANCE = new ClockGuardTransformer + /** + * Split expression into expressions, which used as parallel edges are equivalent to the original. + * Clock comparisons may only be in the top level of the expression by itself or in a top level `and` expression. + * + * @param guard expression can only contain: AndExpression, LiteralExpression, NotExpression, OrExpression, + * PredicateExpression, ReferenceExpression + * + * @return List of expressions. May be empty if all created expressions are definitely false. + */ def List splitByDisjunction(Expression guard) { val clone = guard.clone - val preservedClone = guard.clone val transformed = clone.toDnfChecked - logger.log(Level.INFO, '''Before: «preservedClone.serialize»; After: «transformed.serialize»''') + logger.log(Level.INFO, '''Before: «guard.serialize»; After: «transformed.serialize»''') if (transformed instanceof OrExpression) { return transformed.operands.reject[it.isDefinitelyFalseExpression].clone } return #[transformed] } - + + /** + * Function to transform expression into DNF form only if it contains references to clock variables. + * + * @param exp Limitations listed at splitByDisjunction + */ private def Expression toDnfChecked(Expression exp) { if (exp.containsClockReference) { return toDnf(exp) @@ -48,6 +70,10 @@ class ClockGuardTransformer { return exp.clone } + /** + * Dispatch recursive function (through toDnfChecked) to bring an expression into DNF form. + * @param exp Limitations listed at splitByDisjunction + */ private dispatch def Expression toDnf(Expression exp) { throw new IllegalArgumentException("Unhandled parameter types: " + exp); } @@ -85,6 +111,8 @@ class ClockGuardTransformer { private dispatch def Expression toDnf(OrExpression expr) { val operands = expr.operands.map[toDnfChecked] + // Bring up inner `or`s + // A or (B or C) => A or B or C val flattenedOperands = operands.flatMap [ if (it instanceof OrExpression) { return it.operands @@ -100,9 +128,9 @@ class ClockGuardTransformer { /** * This method may be used to distribute ANDs over ORs. * - * @param operands list of operands + * @param operands list of operands of the original AND expression. Doesn't have to contain any ORs. * - * @returns if distribution was necessary an `OrExpression`, otherwise an #[list.head]`AndExpression` + * @returns if distribution was necessary an `OrExpression`, otherwise an `AndExpression` */ private def Expression distributeAnd(List operands) { if (!operands.exists[it instanceof OrExpression]) { @@ -152,12 +180,18 @@ class ClockGuardTransformer { ].clone } + /** + * Check if the expression contains a reference to a clock variable + */ private def containsClockReference(Expression expression) { return expression !== null && expression.getSelfAndAllContentsOfType(DirectReferenceExpression).exists [ it.clock ] } + /** + * Check if the referenced variable is a clock + */ private def boolean isClock(DirectReferenceExpression expr) { val declaration = expr.declaration if (declaration instanceof VariableDeclaration) { From 8fe135d00caca6211cb3852547911187f611d918 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Bence=20T=C3=B3th?= Date: Thu, 3 Apr 2025 14:11:23 +0200 Subject: [PATCH 10/13] cleanup debug statements --- .../ClockGuardTransformer.xtend | 23 ++++++++----------- 1 file changed, 10 insertions(+), 13 deletions(-) diff --git a/plugins/xsts/hu.bme.mit.gamma.xsts.uppaal.transformation/src/hu/bme/mit/gamma/xsts/uppaal/transformation/ClockGuardTransformer.xtend b/plugins/xsts/hu.bme.mit.gamma.xsts.uppaal.transformation/src/hu/bme/mit/gamma/xsts/uppaal/transformation/ClockGuardTransformer.xtend index 4e82a05ed..07fb32846 100644 --- a/plugins/xsts/hu.bme.mit.gamma.xsts.uppaal.transformation/src/hu/bme/mit/gamma/xsts/uppaal/transformation/ClockGuardTransformer.xtend +++ b/plugins/xsts/hu.bme.mit.gamma.xsts.uppaal.transformation/src/hu/bme/mit/gamma/xsts/uppaal/transformation/ClockGuardTransformer.xtend @@ -1,24 +1,22 @@ package hu.bme.mit.gamma.xsts.uppaal.transformation -import hu.bme.mit.gamma.expression.model.Expression -import java.util.List -import hu.bme.mit.gamma.expression.model.NotExpression -import hu.bme.mit.gamma.util.GammaEcoreUtil import hu.bme.mit.gamma.expression.model.AndExpression +import hu.bme.mit.gamma.expression.model.ClockVariableDeclarationAnnotation +import hu.bme.mit.gamma.expression.model.DirectReferenceExpression +import hu.bme.mit.gamma.expression.model.Expression import hu.bme.mit.gamma.expression.model.ExpressionModelFactory -import hu.bme.mit.gamma.expression.model.OrExpression -import hu.bme.mit.gamma.expression.model.ReferenceExpression import hu.bme.mit.gamma.expression.model.LiteralExpression +import hu.bme.mit.gamma.expression.model.NotExpression +import hu.bme.mit.gamma.expression.model.OrExpression import hu.bme.mit.gamma.expression.model.PredicateExpression +import hu.bme.mit.gamma.expression.model.ReferenceExpression +import hu.bme.mit.gamma.expression.model.VariableDeclaration +import hu.bme.mit.gamma.expression.util.ExpressionEvaluator import hu.bme.mit.gamma.expression.util.ExpressionNegator import hu.bme.mit.gamma.expression.util.ExpressionSerializer +import hu.bme.mit.gamma.util.GammaEcoreUtil +import java.util.List import java.util.logging.Logger -import java.util.logging.Level -import hu.bme.mit.gamma.expression.util.ExpressionEvaluator -import hu.bme.mit.gamma.expression.model.DirectReferenceExpression -import hu.bme.mit.gamma.expression.model.VariableDeclaration -import hu.bme.mit.gamma.expression.model.ClockVariableDeclarationAnnotation - /** * A utility class that brings guard expressions to DNF form in regard to clock variables. @@ -51,7 +49,6 @@ class ClockGuardTransformer { def List splitByDisjunction(Expression guard) { val clone = guard.clone val transformed = clone.toDnfChecked - logger.log(Level.INFO, '''Before: «guard.serialize»; After: «transformed.serialize»''') if (transformed instanceof OrExpression) { return transformed.operands.reject[it.isDefinitelyFalseExpression].clone } From dbd13e797c665885e9eea2296a1f3f571fafd6fe Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Bence=20T=C3=B3th?= Date: Fri, 4 Apr 2025 00:08:19 +0200 Subject: [PATCH 11/13] Formatting --- .../xsts/uppaal/transformation/ClockGuardTransformer.xtend | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/plugins/xsts/hu.bme.mit.gamma.xsts.uppaal.transformation/src/hu/bme/mit/gamma/xsts/uppaal/transformation/ClockGuardTransformer.xtend b/plugins/xsts/hu.bme.mit.gamma.xsts.uppaal.transformation/src/hu/bme/mit/gamma/xsts/uppaal/transformation/ClockGuardTransformer.xtend index 07fb32846..e72bc572c 100644 --- a/plugins/xsts/hu.bme.mit.gamma.xsts.uppaal.transformation/src/hu/bme/mit/gamma/xsts/uppaal/transformation/ClockGuardTransformer.xtend +++ b/plugins/xsts/hu.bme.mit.gamma.xsts.uppaal.transformation/src/hu/bme/mit/gamma/xsts/uppaal/transformation/ClockGuardTransformer.xtend @@ -34,7 +34,9 @@ class ClockGuardTransformer { protected final extension ExpressionSerializer expressionSerializer = ExpressionSerializer.INSTANCE protected final Logger logger = Logger.getLogger("GammaLogger") - /// Singleton class instance + /** + * Singleton class instance + */ public static final ClockGuardTransformer INSTANCE = new ClockGuardTransformer /** @@ -54,7 +56,7 @@ class ClockGuardTransformer { } return #[transformed] } - + /** * Function to transform expression into DNF form only if it contains references to clock variables. * From bc52d878900d289dde2070895f6330a261a54ff4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Bence=20T=C3=B3th?= Date: Wed, 9 Apr 2025 21:53:48 +0200 Subject: [PATCH 12/13] refactor edge splitting to a separate function --- .../transformation/CfaActionTransformer.xtend | 50 +++++++------------ 1 file changed, 18 insertions(+), 32 deletions(-) diff --git a/plugins/xsts/hu.bme.mit.gamma.xsts.uppaal.transformation/src/hu/bme/mit/gamma/xsts/uppaal/transformation/CfaActionTransformer.xtend b/plugins/xsts/hu.bme.mit.gamma.xsts.uppaal.transformation/src/hu/bme/mit/gamma/xsts/uppaal/transformation/CfaActionTransformer.xtend index 6351d52ef..78e1aa1c1 100644 --- a/plugins/xsts/hu.bme.mit.gamma.xsts.uppaal.transformation/src/hu/bme/mit/gamma/xsts/uppaal/transformation/CfaActionTransformer.xtend +++ b/plugins/xsts/hu.bme.mit.gamma.xsts.uppaal.transformation/src/hu/bme/mit/gamma/xsts/uppaal/transformation/CfaActionTransformer.xtend @@ -37,6 +37,7 @@ import static hu.bme.mit.gamma.uppaal.util.XstsNamings.* import static extension de.uni_paderborn.uppaal.derivedfeatures.UppaalModelDerivedFeatures.* import static extension hu.bme.mit.gamma.expression.derivedfeatures.ExpressionModelDerivedFeatures.* import static extension java.lang.Math.* +import hu.bme.mit.gamma.expression.model.Expression class CfaActionTransformer { @@ -145,18 +146,7 @@ class CfaActionTransformer { } protected def dispatch Location transformAction(AssumeAction action, Location source) { - val target = createLocation(source.parentTemplate) => [ - it.name = nextCommittedLocationName - it.locationTimeKind = LocationKind.COMMITED - ] - val guards = action.assumption.splitByDisjunction.map[transform] - for (guard : guards) { - source.createEdge(target) => [ - it.guard = guard - ] - } - - return target + return action.assumption.transformGuard(source) } protected def dispatch Location transformAction(SequentialAction action, Location source) { @@ -200,30 +190,12 @@ class CfaActionTransformer { val negativeCondition = condition.clone .createNotExpression - val thenGuardTarget = createLocation(source.parentTemplate) => [ - it.name = nextCommittedLocationName - it.locationTimeKind = LocationKind.COMMITED - ] - val thenGuards = positiveCondition.splitByDisjunction.map[transform] - for (guard : thenGuards) { - source.createEdge(thenGuardTarget) => [ - it.guard = guard - ] - } + val thenGuardTarget = positiveCondition.transformGuard(source) val thenAction = action.then val thenActionTarget = thenAction.transformAction(thenGuardTarget) - val elseGuardTarget = createLocation(source.parentTemplate) => [ - it.name = nextCommittedLocationName - it.locationTimeKind = LocationKind.COMMITED - ] - val elseGuards = negativeCondition.splitByDisjunction.map[transform] - for (guard : elseGuards) { - source.createEdge(elseGuardTarget) => [ - it.guard = guard - ] - } + val elseGuardTarget = negativeCondition.transformGuard(source) val elseAction = action.^else val elseActionTarget = (elseAction !== null) ? elseAction.transformAction(elseGuardTarget) : elseGuardTarget @@ -295,6 +267,20 @@ class CfaActionTransformer { } } + protected def Location transformGuard(Expression guard, Location source){ + val target = createLocation(source.parentTemplate) => [ + it.name = nextCommittedLocationName + it.locationTimeKind = LocationKind.COMMITED + ] + val transformedGuards = guard.splitByDisjunction.map[transform] + for (transformedGuard : transformedGuards) { + source.createEdge(target) => [ + it.guard = transformedGuard + ] + } + return target + } + // // Variable binding // // def getVariableBindings() { From 8d1b81b12b51785afb6598f2480b9eb3b83b1c68 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Bence=20T=C3=B3th?= Date: Wed, 23 Apr 2025 22:17:08 +0200 Subject: [PATCH 13/13] Add copyright notice --- .../transformation/ClockGuardTransformer.xtend | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/plugins/xsts/hu.bme.mit.gamma.xsts.uppaal.transformation/src/hu/bme/mit/gamma/xsts/uppaal/transformation/ClockGuardTransformer.xtend b/plugins/xsts/hu.bme.mit.gamma.xsts.uppaal.transformation/src/hu/bme/mit/gamma/xsts/uppaal/transformation/ClockGuardTransformer.xtend index e72bc572c..521254281 100644 --- a/plugins/xsts/hu.bme.mit.gamma.xsts.uppaal.transformation/src/hu/bme/mit/gamma/xsts/uppaal/transformation/ClockGuardTransformer.xtend +++ b/plugins/xsts/hu.bme.mit.gamma.xsts.uppaal.transformation/src/hu/bme/mit/gamma/xsts/uppaal/transformation/ClockGuardTransformer.xtend @@ -1,4 +1,14 @@ -package hu.bme.mit.gamma.xsts.uppaal.transformation +/******************************************************************************** + * Copyright (c) 2025 Contributors to the Gamma project + * + * All rights reserved. This program and the accompanying materials + * are made available under the terms of the Eclipse Public License v1.0 + * which accompanies this distribution, and is available at + * http://www.eclipse.org/legal/epl-v10.html + * + * SPDX-License-Identifier: EPL-1.0 + ********************************************************************************/ + package hu.bme.mit.gamma.xsts.uppaal.transformation import hu.bme.mit.gamma.expression.model.AndExpression import hu.bme.mit.gamma.expression.model.ClockVariableDeclarationAnnotation