From 87bce928b11fae67ff4d88aad71189459bbed616 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Fri, 17 Jul 2015 07:57:12 +0000 Subject: [PATCH] Code tidy git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10352 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/MDPModelChecker.java | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/prism/src/explicit/MDPModelChecker.java b/prism/src/explicit/MDPModelChecker.java index c72016ae..e8805dab 100644 --- a/prism/src/explicit/MDPModelChecker.java +++ b/prism/src/explicit/MDPModelChecker.java @@ -83,12 +83,12 @@ public class MDPModelChecker extends ProbModelChecker // For LTL model checking routines mcLtl = new LTLModelChecker(this); + // Build product of MDP and automaton AcceptanceType[] allowedAcceptance = { AcceptanceType.RABIN, AcceptanceType.GENERALIZED_RABIN, AcceptanceType.REACH }; - product = mcLtl.constructProductMDP(this, (MDP)model, expr, statesOfInterest, allowedAcceptance); // Output product, if required @@ -150,11 +150,11 @@ public class MDPModelChecker extends ProbModelChecker // For LTL model checking routines mcLtl = new LTLModelChecker(this); + // Build product of MDP and automaton AcceptanceType[] allowedAcceptance = { AcceptanceType.RABIN, AcceptanceType.REACH }; - product = mcLtl.constructProductMDP(this, (MDP)model, expr, statesOfInterest, allowedAcceptance); // Adapt reward info to product model