From 56c484d39024b6a52c3a62d52327a7bab5c0179e Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Sun, 22 Dec 2013 01:01:06 +0000 Subject: [PATCH] Code re-factoring in NondetModelChecker. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@7735 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/NondetModelChecker.java | 21 ++++++++------------- 1 file changed, 8 insertions(+), 13 deletions(-) diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java index 0218f695..9ccf5378 100644 --- a/prism/src/prism/NondetModelChecker.java +++ b/prism/src/prism/NondetModelChecker.java @@ -111,12 +111,9 @@ public class NondetModelChecker extends NonProbModelChecker PrismNative.setExportAdvFilename(prism.getExportAdvFilename()); } - // ----------------------------------------------------------------------------------- - // Check a property, i.e. an expression - // ----------------------------------------------------------------------------------- - - // Check expression (recursive) + // Model checking functions + @Override public StateValues checkExpression(Expression expr) throws PrismException { StateValues res; @@ -153,12 +150,9 @@ public class NondetModelChecker extends NonProbModelChecker return res; } - // ----------------------------------------------------------------------------------- - // Check method for each operator - // ----------------------------------------------------------------------------------- - - // P operator - + /** + * Model check a P operator expression and return the values for all states. + */ protected StateValues checkExpressionProb(ExpressionProb expr) throws PrismException { Expression pb; // probability bound (expression) @@ -227,8 +221,9 @@ public class NondetModelChecker extends NonProbModelChecker } } - // R operator - + /** + * Model check an R operator expression and return the values for all states. + */ protected StateValues checkExpressionReward(ExpressionReward expr) throws PrismException { Object rs; // reward struct index