From acc6287639e924f20a5b7bc8177d4ddecd4686fc Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Fri, 19 Aug 2016 14:44:00 +0000 Subject: [PATCH] New convenience method in prism.Prism API for model checking a property specified as a string, with parsing done automatically. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11657 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/Prism.java | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index bc7e3fb6..1a5fd6f2 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -2750,6 +2750,24 @@ public class Prism extends PrismComponent implements PrismSettingsListener tmpLog.close(); } + /** + * Perform model checking of a property on the currently loaded model and return result. + * Here, the property is passed as a string and parsed first. Usually, you would use the other + * model checking methods which assume you have already parsed the property separately. + * This is just a simplified method for convenience. The property string can in fact be a whole + * properties file, e.g. you can define labels/constants/etc. too, but an exception will be + * thrown if there is more than one property present. + * @param propertyString The property (in fact properties file) to check as a string + */ + public Result modelCheck(String propertyString) throws PrismException + { + PropertiesFile propertiesFile = parsePropertiesString(currentModelGenerator, propertyString); + if (propertiesFile.getNumProperties() != 1) { + throw new PrismException("There should be exactly one property to check (there are " + propertiesFile.getNumProperties() + ")"); + } + return modelCheck(propertiesFile, propertiesFile.getPropertyObject(0)); + } + /** * Perform model checking of a property on the currently loaded model and return result. * @param propertiesFile Parent property file of property (for labels/constants/...)