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

@@ -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");
 			}

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.");
 		}
 	}
 

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);

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)