From 786d2ac6a820b6b0c0ad4e58effd083610707110 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Thu, 27 Sep 2012 08:57:20 +0000 Subject: [PATCH] Tidy: Auto-format. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5702 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/LTLModelChecker.java | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/prism/src/prism/LTLModelChecker.java b/prism/src/prism/LTLModelChecker.java index 444e5355..3bf9dbae 100644 --- a/prism/src/prism/LTLModelChecker.java +++ b/prism/src/prism/LTLModelChecker.java @@ -58,7 +58,7 @@ public class LTLModelChecker { return LTL2RabinLibrary.convertLTLFormulaToDRA(ltl); } - + /** * Extract maximal state formula from an LTL path formula, model check them (with passed in model checker) and * replace them with ExpressionLabel objects L0, L1, etc. Expression passed in is modified directly, but the result @@ -304,7 +304,7 @@ public class LTLModelChecker JDD.Ref(model.getStart()); newStart = JDD.And(model.getStart(), newStart); modelProd.setStart(newStart); - + // Reference DRA DD vars (if being returned) if (draDDRowVarsCopy != null) draDDRowVarsCopy.refAll(); @@ -520,7 +520,7 @@ public class LTLModelChecker JDD.Ref(model.getStart()); newStart = JDD.And(model.getStart(), newStart); modelProd.setStart(newStart); - + //try { prism.exportStatesToFile(modelProd, Prism.EXPORT_PLAIN, new java.io.File("prod.sta")); } //catch (java.io.FileNotFoundException e) {} @@ -539,7 +539,8 @@ public class LTLModelChecker * * @return a referenced mask BDD over trans */ - public JDDNode buildTransMask(DRA dra, Vector labelDDs, JDDVars allDDRowVars, JDDVars allDDColVars, JDDVars draDDRowVars, JDDVars draDDColVars) + public JDDNode buildTransMask(DRA dra, Vector labelDDs, JDDVars allDDRowVars, JDDVars allDDColVars, JDDVars draDDRowVars, + JDDVars draDDColVars) { JDDNode draMask, label, exprBDD, transition; int i, j, k, numAPs, numStates, numEdges;