Browse Source

(HOA path) explicit MDP checker: allow Streett acceptance for LTL model checking

accumulation-v4.7
Joachim Klein 7 years ago
committed by Joachim Klein
parent
commit
e7759bfe37
  1. 3
      prism/src/explicit/MDPModelChecker.java

3
prism/src/explicit/MDPModelChecker.java

@ -102,10 +102,11 @@ public class MDPModelChecker extends ProbModelChecker
// Build product of MDP and automaton
AcceptanceType[] allowedAcceptance = {
AcceptanceType.REACH,
AcceptanceType.BUCHI,
AcceptanceType.RABIN,
AcceptanceType.GENERALIZED_RABIN,
AcceptanceType.REACH
AcceptanceType.STREETT
};
product = mcLtl.constructProductMDP(this, (MDP)model, expr, statesOfInterest, allowedAcceptance);

Loading…
Cancel
Save