From d48f5c84a293f2e45de92d42ae5bf71957d241d9 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Sat, 25 Feb 2012 21:11:02 +0000 Subject: [PATCH] Digital clocks translation adds an "invariants" label, equal to the conjunction of module invariants. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4725 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/pta/DigitalClocks.java | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/prism/src/pta/DigitalClocks.java b/prism/src/pta/DigitalClocks.java index 87324e45..637cb25d 100644 --- a/prism/src/pta/DigitalClocks.java +++ b/prism/src/pta/DigitalClocks.java @@ -60,6 +60,8 @@ public class DigitalClocks private ComputeClockInformation cci; // String to be used for time action private String timeAction; + // Some invariant info + private Expression allInVariants = null; // Translated model file private ModulesFile mf; @@ -178,6 +180,8 @@ public class DigitalClocks }); // Add time command based on invariant for each module + // Also build an "invariants" label, as we go + allInVariants = null; mf = (ModulesFile) mf.accept(new ASTTraverseModify() { public Object visit(Module e) throws PrismLangException @@ -192,6 +196,9 @@ public class DigitalClocks // Get (clock) invariant for module; create default if none invar = e.getInvariant(); invar = (invar == null) ? Expression.True() : invar.deepCopy(); + // Collect invariant for "invariants" label + if (!Expression.isTrue(invar)) + allInVariants = (allInVariants == null) ? invar.deepCopy() : Expression.And(allInVariants, invar.deepCopy()); // Replace all clocks x with x+1 in invariant invar = (Expression) invar.accept(new ASTTraverseModify() { @@ -231,6 +238,8 @@ public class DigitalClocks return e; } }); + // Add "invariants" label + mf.getLabelList().addLabel(new ExpressionIdent("invariants"), allInVariants == null ? Expression.True() : allInVariants); // Change the type of any clock variable references to int // and scale the variable appropriately, if required