From 232b02d7f4315d0171513b7be60b928e8ca3a56f Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Fri, 10 Feb 2012 17:30:51 +0000 Subject: [PATCH] Change PrismTest to use new Prism API. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4580 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/PrismTest.java | 27 +++++++++------------------ 1 file changed, 9 insertions(+), 18 deletions(-) diff --git a/prism/src/prism/PrismTest.java b/prism/src/prism/PrismTest.java index 87e65a8e..cd610ecb 100644 --- a/prism/src/prism/PrismTest.java +++ b/prism/src/prism/PrismTest.java @@ -33,6 +33,7 @@ import parser.ast.*; /** * Example class demonstrating how to control PRISM programmatically, * i.e. through the "API" exposed by the class prism.Prism. + * (this now uses the newer version of the API, released after PRISM 4.0.3) * Test like this: * PRISM_MAINCLASS=prism.PrismTest bin/prism ../prism-examples/polling/poll2.sm ../prism-examples/polling/poll3.sm */ @@ -58,40 +59,30 @@ public class PrismTest prism = new Prism(mainLog, mainLog); prism.initialise(); - // Parse build model 1 + // Parse/load model 1 + // NB: no need to build explicitly - it will be done if/when neeed modulesFile = prism.parseModelFile(new File(args[0])); - modulesFile.setUndefinedConstants(null); - model = prism.buildModel(modulesFile); + prism.loadPRISMModel(modulesFile); // Parse a prop, check on model 1 propertiesFile = prism.parsePropertiesString(modulesFile, "P=?[F<=0.1 s1=1]"); - propertiesFile.setUndefinedConstants(null); - result = prism.modelCheck(model, propertiesFile, propertiesFile.getProperty(0)); + result = prism.modelCheck(propertiesFile, propertiesFile.getProperty(0), null); System.out.println(result.getResult()); // Parse another prop, check on model 1 propertiesFile = prism.parsePropertiesString(modulesFile, "P=?[F<=0.1 s1=1]"); - propertiesFile.setUndefinedConstants(null); - result = prism.modelCheck(model, propertiesFile, propertiesFile.getProperty(0)); + result = prism.modelCheck(propertiesFile, propertiesFile.getProperty(0), null); System.out.println(result.getResult()); - // Clear model 1 - model.clear(); - - // Parse build model 2 + // Parse/load model 2 modulesFile = prism.parseModelFile(new File(args[1])); - modulesFile.setUndefinedConstants(null); - model = prism.buildModel(modulesFile); + prism.loadPRISMModel(modulesFile); // Parse a prop, check on model 2 propertiesFile = prism.parsePropertiesString(modulesFile, "P=?[F<=0.1 s1=1]"); - propertiesFile.setUndefinedConstants(null); - result = prism.modelCheck(model, propertiesFile, propertiesFile.getProperty(0)); + result = prism.modelCheck(propertiesFile, propertiesFile.getProperty(0), null); System.out.println(result.getResult()); - // Clear model 2 - model.clear(); - // Close down prism.closeDown(); }