From 34f1645c4ec064cd6cd9f9b639120f2ccabe1730 Mon Sep 17 00:00:00 2001 From: Yann Thierry-Mieg Date: Sun, 5 May 2024 17:10:37 +0200 Subject: [PATCH] pulled up toPredicates ; TODO : refactor to external helper class --- .../move/gal/structural/ISparsePetriNet.java | 80 +++++++++++++++++++ .../move/gal/structural/SparsePetriNet.java | 70 +--------------- 2 files changed, 81 insertions(+), 69 deletions(-) diff --git a/fr.lip6.move.gal.structural/src/fr/lip6/move/gal/structural/ISparsePetriNet.java b/fr.lip6.move.gal.structural/src/fr/lip6/move/gal/structural/ISparsePetriNet.java index 423a19b3bb..8dc4bfa229 100644 --- a/fr.lip6.move.gal.structural/src/fr/lip6/move/gal/structural/ISparsePetriNet.java +++ b/fr.lip6.move.gal.structural/src/fr/lip6/move/gal/structural/ISparsePetriNet.java @@ -1,8 +1,17 @@ package fr.lip6.move.gal.structural; +import java.util.ArrayList; import java.util.BitSet; +import java.util.HashSet; import java.util.List; +import java.util.Set; +import java.util.logging.Logger; +import android.util.SparseIntArray; +import fr.lip6.move.gal.structural.expr.BinOp; +import fr.lip6.move.gal.structural.expr.Expression; +import fr.lip6.move.gal.structural.expr.NaryOp; +import fr.lip6.move.gal.structural.expr.Op; import fr.lip6.move.gal.util.IntMatrixCol; public interface ISparsePetriNet { @@ -29,4 +38,75 @@ public interface ISparsePetriNet { void setSafe(boolean isSafe); + default void toPredicates(List properties) { + for (Property prop : properties) { + prop.setBody(replacePredicates(prop.getBody())); + } + } + + default Expression replacePredicates(Expression expr) { + if (expr == null) { + return expr; + } else if (expr instanceof BinOp) { + BinOp bin = (BinOp) expr; + if (bin.getOp() == Op.DEAD) { + return Expression.not(Expression.op(Op.EX, Expression.constant(true), null)); + } + Expression l = replacePredicates(bin.left); + Expression r = replacePredicates(bin.right); + if (l == bin.left && r == bin.right) { + return expr; + } + return Expression.op(bin.op, l, r); + } else if (expr instanceof NaryOp) { + NaryOp nop = (NaryOp) expr; + List resc = new ArrayList<>(); + if (expr.getOp() == Op.CARD || expr.getOp() == Op.BOUND) { + for (Expression child : nop.getChildren()) { + if (child.getOp() == Op.PLACEREF) { + resc.add(Expression.var(child.getValue())); + } else { + resc.add(child); + } + } + return Expression.nop(Op.ADD, resc); + } else if (expr.getOp() == Op.ENABLED) { + Set pres = new HashSet<>(); + int skipped = 0; + for (Expression child : nop.getChildren()) { + if (child.getOp() == Op.TRANSREF) { + int tid = child.getValue(); + if (!pres.add(getFlowPT().getColumn(tid))) { + skipped++; + } + } + } + if (skipped > 0) { + Logger.getLogger("fr.lip6.move.gal").info("Reduced "+skipped+" identical enabling conditions."); + } + for (SparseIntArray pre : pres) { + List conds = new ArrayList<>(); + for (int i=0,ie=pre.size();i resc = new ArrayList<>(); - if (expr.getOp() == Op.CARD || expr.getOp() == Op.BOUND) { - for (Expression child : nop.getChildren()) { - if (child.getOp() == Op.PLACEREF) { - resc.add(Expression.var(child.getValue())); - } else { - resc.add(child); - } - } - return Expression.nop(Op.ADD, resc); - } else if (expr.getOp() == Op.ENABLED) { - Set pres = new HashSet<>(); - int skipped = 0; - for (Expression child : nop.getChildren()) { - if (child.getOp() == Op.TRANSREF) { - int tid = child.getValue(); - if (!pres.add(flowPT.getColumn(tid))) { - skipped++; - } - } - } - if (skipped > 0) { - Logger.getLogger("fr.lip6.move.gal").info("Reduced "+skipped+" identical enabling conditions."); - } - for (SparseIntArray pre : pres) { - List conds = new ArrayList<>(); - for (int i=0,ie=pre.size();i