From bdb7b8be608d028597335eee504f1d947d56b38e Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Mon, 17 Mar 2008 07:52:18 +0000 Subject: [PATCH] Enabled steady-state properties for DTMCs. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@666 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/parser/visitor/CheckValid.java | 6 ------ prism/src/prism/PrismCL.java | 4 ++-- prism/src/userinterface/model/GUIMultiModel.java | 2 +- .../model/computation/ComputeSteadyStateThread.java | 2 +- 4 files changed, 4 insertions(+), 10 deletions(-) diff --git a/prism/src/parser/visitor/CheckValid.java b/prism/src/parser/visitor/CheckValid.java index 30aa1928..ddaac985 100644 --- a/prism/src/parser/visitor/CheckValid.java +++ b/prism/src/parser/visitor/CheckValid.java @@ -44,9 +44,6 @@ public class CheckValid extends ASTTraverse public void visitPost(ExpressionSS e) throws PrismLangException { - if (modelType == ModulesFile.PROBABILISTIC) { - throw new PrismLangException("The S operator cannot be used for DTMCs"); - } if (modelType == ModulesFile.NONDETERMINISTIC) { throw new PrismLangException("The S operator cannot be used for MDPs"); } @@ -55,9 +52,6 @@ public class CheckValid extends ASTTraverse public void visitPost(PathExpressionTemporal e) throws PrismLangException { if (e.getOperator() == PathExpressionTemporal.R_S) { - if (modelType == ModulesFile.PROBABILISTIC) { - throw new PrismLangException("Steady-state reward properties cannot be used for DTMCs"); - } if (modelType == ModulesFile.NONDETERMINISTIC) { throw new PrismLangException("Steady-state reward properties cannot be used for MDPs"); } diff --git a/prism/src/prism/PrismCL.java b/prism/src/prism/PrismCL.java index 900f65be..cb01b6fb 100644 --- a/prism/src/prism/PrismCL.java +++ b/prism/src/prism/PrismCL.java @@ -679,11 +679,11 @@ public class PrismCL private void doSteadyState() throws PrismException { // compute steady-state probabilities - if (model instanceof StochModel) { + if (model instanceof StochModel || model instanceof ProbModel) { prism.doSteadyState(model); } else { - mainLog.println("\nWarning: Steady-state probabilities only computed for CTMC models."); + mainLog.println("\nWarning: Steady-state probabilities only computed for DTMCs/CTMCs."); } } diff --git a/prism/src/userinterface/model/GUIMultiModel.java b/prism/src/userinterface/model/GUIMultiModel.java index 0f25be2b..6fe5b816 100644 --- a/prism/src/userinterface/model/GUIMultiModel.java +++ b/prism/src/userinterface/model/GUIMultiModel.java @@ -136,7 +136,7 @@ public class GUIMultiModel extends GUIPlugin implements PrismSettingsListener viewStateRewards.setEnabled(!computing); viewTransRewards.setEnabled(!computing); viewPrismCode.setEnabled(!computing && handler.getParseState() == GUIMultiModelTree.TREE_SYNCHRONIZED_GOOD); - computeSS.setEnabled(!computing && (handler.getParsedModelType() == ModulesFile.STOCHASTIC)); + computeSS.setEnabled(!computing && (handler.getParsedModelType() == ModulesFile.STOCHASTIC || handler.getParsedModelType() == ModulesFile.PROBABILISTIC)); computeTr.setEnabled(!computing && (handler.getParsedModelType() == ModulesFile.STOCHASTIC)); exportStatesPlain.setEnabled(!computing); exportStatesMatlab.setEnabled(!computing); diff --git a/prism/src/userinterface/model/computation/ComputeSteadyStateThread.java b/prism/src/userinterface/model/computation/ComputeSteadyStateThread.java index c8887589..5048141d 100644 --- a/prism/src/userinterface/model/computation/ComputeSteadyStateThread.java +++ b/prism/src/userinterface/model/computation/ComputeSteadyStateThread.java @@ -64,7 +64,7 @@ public class ComputeSteadyStateThread extends GUIComputationThread //Do Computation try { - if(!(computeThis instanceof StochModel)) throw new PrismException("Can only compute steady-state probabilities for CTMCs"); + if(!(computeThis instanceof StochModel || computeThis instanceof ProbModel)) throw new PrismException("Can only compute steady-state probabilities for CTMCs"); prism.doSteadyState(computeThis); } catch(PrismException e)