Browse Source
Add initial support to Prism API to load ModelGenerator objects + some associated changes in infrastructure + a test case.
Add initial support to Prism API to load ModelGenerator objects + some associated changes in infrastructure + a test case.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10996 bbc10eb1-c90d-0410-af57-cb519fbb1720master
Dave Parker
11 years ago
8 changed files with 349 additions and 90 deletions
-
39prism/src/parser/PrismParser.java
-
17prism/src/parser/PrismParser.jj
-
1prism/src/parser/PrismParserTokenManager.java
-
26prism/src/parser/ast/PropertiesFile.java
-
34prism/src/parser/visitor/PropertiesSemanticCheck.java
-
113prism/src/prism/Prism.java
-
8prism/src/prism/PrismCL.java
-
201prism/src/prism/TestModelGenerator.java
@ -0,0 +1,201 @@ |
|||||
|
//============================================================================== |
||||
|
// |
||||
|
// Copyright (c) 2002- |
||||
|
// Authors: |
||||
|
// * Dave Parker <d.a.parker@cs.bham.ac.uk> (University of Birmingham/Oxford) |
||||
|
// |
||||
|
//------------------------------------------------------------------------------ |
||||
|
// |
||||
|
// This file is part of PRISM. |
||||
|
// |
||||
|
// PRISM is free software; you can redistribute it and/or modify |
||||
|
// it under the terms of the GNU General Public License as published by |
||||
|
// the Free Software Foundation; either version 2 of the License, or |
||||
|
// (at your option) any later version. |
||||
|
// |
||||
|
// PRISM is distributed in the hope that it will be useful, |
||||
|
// but WITHOUT ANY WARRANTY; without even the implied warranty of |
||||
|
// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the |
||||
|
// GNU General Public License for more details. |
||||
|
// |
||||
|
// You should have received a copy of the GNU General Public License |
||||
|
// along with PRISM; if not, write to the Free Software Foundation, |
||||
|
// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA |
||||
|
// |
||||
|
//============================================================================== |
||||
|
|
||||
|
package prism; |
||||
|
|
||||
|
import java.io.File; |
||||
|
import java.io.FileNotFoundException; |
||||
|
|
||||
|
import parser.State; |
||||
|
import parser.VarList; |
||||
|
import parser.ast.Declaration; |
||||
|
import parser.ast.DeclarationInt; |
||||
|
import parser.ast.Expression; |
||||
|
import parser.ast.PropertiesFile; |
||||
|
import explicit.ConstructModel; |
||||
|
import explicit.DTMCModelChecker; |
||||
|
|
||||
|
public class TestModelGenerator extends DefaultModelGenerator |
||||
|
{ |
||||
|
protected State exploreState; |
||||
|
protected int x; |
||||
|
protected int n; |
||||
|
|
||||
|
public TestModelGenerator(int n) |
||||
|
{ |
||||
|
this.n = n; |
||||
|
} |
||||
|
|
||||
|
@Override |
||||
|
public ModelType getModelType() |
||||
|
{ |
||||
|
return ModelType.DTMC; |
||||
|
} |
||||
|
|
||||
|
@Override |
||||
|
public int getNumLabels() |
||||
|
{ |
||||
|
return 1; |
||||
|
} |
||||
|
|
||||
|
@Override |
||||
|
public String getLabelName(int i) throws PrismException |
||||
|
{ |
||||
|
if (i == 0) { |
||||
|
return "goal"; |
||||
|
} else { |
||||
|
throw new PrismException("Label number \"" + i + "\" not defined"); |
||||
|
} |
||||
|
} |
||||
|
|
||||
|
@Override |
||||
|
public int getLabelIndex(String label) |
||||
|
{ |
||||
|
return ("goal".equals(label)) ? 0 : -1; |
||||
|
} |
||||
|
|
||||
|
@Override |
||||
|
public State getInitialState() throws PrismException |
||||
|
{ |
||||
|
State s = new State(1); |
||||
|
s.varValues[0] = n/2; |
||||
|
return s; |
||||
|
} |
||||
|
|
||||
|
@Override |
||||
|
public void exploreState(State exploreState) throws PrismException |
||||
|
{ |
||||
|
this.exploreState = exploreState; |
||||
|
x = ((Integer) exploreState.varValues[0]).intValue(); |
||||
|
} |
||||
|
|
||||
|
@Override |
||||
|
public State getExploreState() |
||||
|
{ |
||||
|
return exploreState; |
||||
|
} |
||||
|
|
||||
|
@Override |
||||
|
public int getNumChoices() throws PrismException |
||||
|
{ |
||||
|
return 1; |
||||
|
} |
||||
|
|
||||
|
@Override |
||||
|
public int getNumTransitions(int i) throws PrismException |
||||
|
{ |
||||
|
return x > 0 && x < n ? 2 : 1; |
||||
|
} |
||||
|
|
||||
|
@Override |
||||
|
public Object getTransitionAction(int i) throws PrismException |
||||
|
{ |
||||
|
return null; |
||||
|
} |
||||
|
|
||||
|
@Override |
||||
|
public Object getTransitionAction(int i, int offset) throws PrismException |
||||
|
{ |
||||
|
return null; |
||||
|
} |
||||
|
|
||||
|
@Override |
||||
|
public double getTransitionProbability(int i, int offset) throws PrismException |
||||
|
{ |
||||
|
return x > 0 && x < n ? 0.5 : 1.0; |
||||
|
} |
||||
|
|
||||
|
@Override |
||||
|
public State computeTransitionTarget(int i, int offset) throws PrismException |
||||
|
{ |
||||
|
State s = new State(1); |
||||
|
if (x == 0 || x == n) { |
||||
|
s.varValues[i] = x; |
||||
|
} else { |
||||
|
s.varValues[i] = (offset == 0) ? x -1 : x + 1; |
||||
|
} |
||||
|
return s; |
||||
|
} |
||||
|
|
||||
|
@Override |
||||
|
public boolean isLabelTrue(int i) throws PrismException |
||||
|
{ |
||||
|
if (i == 0) { |
||||
|
return x == n; |
||||
|
} else { |
||||
|
throw new PrismException("Label number \"" + i + "\" not defined"); |
||||
|
} |
||||
|
} |
||||
|
|
||||
|
@Override |
||||
|
public VarList createVarList() |
||||
|
{ |
||||
|
VarList varList = new VarList(); |
||||
|
try { |
||||
|
varList.addVar(new Declaration("x", new DeclarationInt(Expression.Int(0), Expression.Int(n))), 0, null); |
||||
|
} catch (PrismLangException e) { |
||||
|
// TODO Auto-generated catch block |
||||
|
e.printStackTrace(); |
||||
|
} |
||||
|
return varList; |
||||
|
} |
||||
|
|
||||
|
public static void main(String args[]) |
||||
|
{ |
||||
|
try { |
||||
|
Prism prism = new Prism(new PrismPrintStreamLog(System.out)); |
||||
|
|
||||
|
int test = 2; |
||||
|
|
||||
|
if (test == 1) { |
||||
|
// Direct usage of model constructor/checker |
||||
|
TestModelGenerator modelGen = new TestModelGenerator(10); |
||||
|
ConstructModel constructModel = new ConstructModel(prism); |
||||
|
explicit.Model model = constructModel.constructModel(modelGen); |
||||
|
model.exportToDotFile(new PrismFileLog("test.dot"), null, true); |
||||
|
DTMCModelChecker mc = new DTMCModelChecker(prism); |
||||
|
PropertiesFile pf = prism.parsePropertiesString(modelGen, "P=? [F \"goal\"]"); |
||||
|
Expression expr = pf.getProperty(0); |
||||
|
Result res = mc.check(model, expr); |
||||
|
System.out.println(res); |
||||
|
} else { |
||||
|
// Perform model construction/checking via Prism |
||||
|
TestModelGenerator modelGen2 = new TestModelGenerator(10); |
||||
|
prism.loadModelGenerator(modelGen2); |
||||
|
prism.exportTransToFile(true, Prism.EXPORT_DOT_STATES, new File("test2.dot")); |
||||
|
PropertiesFile pf = prism.parsePropertiesString(modelGen2, "P=? [F \"goal\"]"); |
||||
|
Expression expr = pf.getProperty(0); |
||||
|
Result res = prism.modelCheck(pf, expr); |
||||
|
System.out.println(res); |
||||
|
} |
||||
|
|
||||
|
} catch (PrismException e) { |
||||
|
System.err.println("Error: " + e.getMessage()); |
||||
|
} catch (FileNotFoundException e) { |
||||
|
System.err.println("Error: " + e.getMessage()); |
||||
|
} |
||||
|
} |
||||
|
} |
||||
Write
Preview
Loading…
Cancel
Save
Reference in new issue