From 1e04c20ca6ade59fa560d30735353de3015055da Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Wed, 6 Mar 2019 15:05:16 +0100 Subject: [PATCH] Fix explicit non-prob LTL checking with experiments MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit We did not perform a required deepCopy of the path expression before checking/replacing maximal state formulas, thus modifying the original expression, which breaks later model checking when doing experiments. Found by Steffen Märcker. --- prism/src/explicit/NonProbModelChecker.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/prism/src/explicit/NonProbModelChecker.java b/prism/src/explicit/NonProbModelChecker.java index 7ee9d96d..6aa36f8d 100644 --- a/prism/src/explicit/NonProbModelChecker.java +++ b/prism/src/explicit/NonProbModelChecker.java @@ -466,7 +466,7 @@ public class NonProbModelChecker extends StateModelChecker LTLModelChecker ltlMC = new LTLModelChecker(this); Vector labelBS = new Vector(); - expr = ltlMC.checkMaximalStateFormulas(this, model, expr, labelBS); + expr = ltlMC.checkMaximalStateFormulas(this, model, expr.deepCopy(), labelBS); // We are doing existential LTL checking: // - Construct an NBA for the LTL formula