From 1071b362e7f8856e53acf4030345d2e5b98beda1 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Mon, 17 Jul 2017 12:46:28 +0000 Subject: [PATCH] explicit LTL, DTMC/MDP product: report product construction time, product statistics git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12046 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/LTLModelChecker.java | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/prism/src/explicit/LTLModelChecker.java b/prism/src/explicit/LTLModelChecker.java index 40e41b32..94833c9c 100644 --- a/prism/src/explicit/LTLModelChecker.java +++ b/prism/src/explicit/LTLModelChecker.java @@ -66,6 +66,7 @@ import automata.DA; import automata.LTL2DA; import common.IterableStateSet; +import common.StopWatch; /** * LTL model checking functionality @@ -275,8 +276,10 @@ public class LTLModelChecker extends PrismComponent // Build product of model and automaton mainLog.println("\nConstructing MC-"+da.getAutomataType()+" product..."); + StopWatch timer = new StopWatch(getLog()); + timer.start("product construction"); LTLProduct product = constructProductModel(da, model, labelBS, statesOfInterest); - mainLog.print("\n" + product.getProductModel().infoStringTable()); + timer.stop("product has " + product.getProductModel().infoString()); return product; } @@ -302,8 +305,10 @@ public class LTLModelChecker extends PrismComponent // Build product of model and automaton mainLog.println("\nConstructing MDP-"+da.getAutomataType()+" product..."); + StopWatch timer = new StopWatch(getLog()); + timer.start("product construction"); LTLProduct product = constructProductModel(da, model, labelBS, statesOfInterest); - mainLog.print("\n" + product.getProductModel().infoStringTable()); + timer.stop("product has " + product.getProductModel().infoString()); return product; }