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..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 { @@ -53,6 +54,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 +146,7 @@ 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 + return action.assumption.transformGuard(source) } protected def dispatch Location transformAction(SequentialAction action, Location source) { @@ -187,23 +186,19 @@ 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 = positiveCondition.transformGuard(source) 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 = negativeCondition.transformGuard(source) val elseAction = action.^else - val elseActionTarget = (elseAction !== null) ? elseAction.transformAction(elseEdgeTarget) : elseEdgeTarget + val elseActionTarget = (elseAction !== null) ? elseAction.transformAction(elseGuardTarget) : elseGuardTarget elseActionTarget.createEdge(thenActionTarget) @@ -272,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() { 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..521254281 --- /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,211 @@ +/******************************************************************************** + * 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 +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.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 + +/** + * 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 + 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") + + /** + * 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 transformed = clone.toDnfChecked + 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) + } + 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); + } + + private dispatch def Expression toDnf(ReferenceExpression exp) { + return exp.clone + } + + private dispatch def Expression toDnf(LiteralExpression exp) { + return exp.clone + } + + private dispatch def Expression toDnf(PredicateExpression exp) { + return exp.clone + } + + private dispatch def Expression toDnf(NotExpression expr) { + val innerExpr = expr.operand + + // not A => not A + // necessary to avoid infinite recursion + if (innerExpr instanceof ReferenceExpression) { + return expr.clone + } + // handles DeMorgan transformations + return innerExpr.negate.toDnfChecked + } + + private dispatch def Expression toDnf(AndExpression expr) { + val operands = expr.operands.map[toDnfChecked] + + return distributeAnd(operands) + } + + 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 + } + return #[it] + ] + + return createOrExpression => [ + it.operands += flattenedOperands.clone + ] + } + + /** + * This method may be used to distribute ANDs over ORs. + * + * @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 `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 + } + + /** + * 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) { + return declaration.annotations.exists[it instanceof ClockVariableDeclarationAnnotation] + } + return false + } +} 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..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 + //nta.transformClockExpressions // CFA transformer handles it // ntaBuilder.instantiateTemplates