From 20a76c622b8576813b7e37e44f12051b07ddf8f9 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Fri, 18 Apr 2008 22:30:14 +0000 Subject: [PATCH] No LTL and fairness. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@761 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/NondetModelChecker.java | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java index f2483337..13c88537 100644 --- a/prism/src/prism/NondetModelChecker.java +++ b/prism/src/prism/NondetModelChecker.java @@ -383,6 +383,16 @@ public class NondetModelChecker extends StateModelChecker int i; long l; + // Can't do LTL and fairness. + // Note: the basic techniques, i.e. DRA product and BSCC reachability work + // (see e.g. Christel's habilitation); the problem is that the current computation + // of satisfying BSCCs is optimised to remove unwanted parts of the product MDP + // which can break fairness (e.g. add new BSCCs). + if (fairness) { + throw new PrismException("Fairness is not supported for LTL properties"); + } + + // For LTL model checking routines mcLtl = new LTLModelChecker(prism, this); // Model check maximal state formulas