From 689de266111c0ac9176ca0a4a49800e18407ff27 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Mon, 26 Jul 2010 21:50:45 +0000 Subject: [PATCH] Comments. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2001 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/Prism.java | 18 ++++++++++++------ 1 file changed, 12 insertions(+), 6 deletions(-) diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index 5f7b4d43..1c7195a1 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -1338,9 +1338,12 @@ public class Prism implements PrismSettingsListener if (file != null) tmpLog.close(); } - // model checking - // returns result or throws an exception in case of error - + /** + * Perform model checking of a property on a model and return result. + * @param model: The model (DTMC, CTMC or MDP) + * @param propertiesFile: Parent property file of property (for labels/constants/...) + * @param expr: The property + */ public Result modelCheck(Model model, PropertiesFile propertiesFile, Expression expr) throws PrismException, PrismLangException { Result res; @@ -1369,9 +1372,12 @@ public class Prism implements PrismSettingsListener return res; } - // model checking for PTAs - // returns result or throws an exception in case of error - + /** + * Perform model checking of a property on a PTA model and return result. + * @param model: The PTA model (language-level) + * @param propertiesFile: Parent property file of property (for labels/constants/...) + * @param expr: The property + */ public Result modelCheckPTA(ModulesFile modulesFile, PropertiesFile propertiesFile, Expression expr) throws PrismException, PrismLangException { PTAModelChecker mcPta;