code: //==============================================================================
  //	
  //	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 java.util.Arrays;
  import java.util.List;
  
  import parser.State;
  import parser.VarList;
  import parser.ast.Declaration;
  import parser.ast.DeclarationInt;
  import parser.ast.Expression;
  import parser.ast.PropertiesFile;
  import parser.type.Type;
  import parser.type.TypeInt;
  import explicit.ConstructModel;
  import explicit.DTMCModelChecker;
  
  public class TestModelGenerator implements ModelGenerator
  {
  	protected State exploreState;
  	protected int x;
  	protected int n;
  	protected List<String> varNames = Arrays.asList("x");
  	protected List<Type> varTypes = Arrays.asList((Type) TypeInt.getInstance());
  
  	public TestModelGenerator(int n)
  	{
  		this.n = n;
  	}
  
  	@Override
  	public ModelType getModelType()
  	{
  		return ModelType.DTMC;
  	}
  
  	@Override
  	public int getNumVars()
  	{
  		return 1;
  	}
  	
  	@Override
  	public List<String> getVarNames()
  	{
  		return varNames;
  	}
  
  	@Override
  	public List<Type> getVarTypes()
  	{
  		return varTypes;
  	}
  
  	@Override
  	public int getNumLabels()
  	{
  		return 1;
  	}
  	
  	@Override
  	public List<String> getLabelNames()
  	{
  		return Arrays.asList("goal");
  	}
  	
  	@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 boolean rewardStructHasTransitionRewards(int i)
  	{
  		return false;
  	}
  
  	@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));
  			prism.setMainLog(new PrismFileLog("stdout"));
  			prism.initialise();
  
  			int test = 2;
  
  			if (test == 1) {
  				// Direct usage of model constructor/checker 
  				TestModelGenerator modelGen = new TestModelGenerator(10);
  				ConstructModel constructModel = new ConstructModel(prism);
  				constructModel.setSortStates(true);
  				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 x=10]");
  				Expression expr = pf.getProperty(0);
  				Result res = prism.modelCheck(pf, expr);
  				System.out.println(res);
  			}
  
  			prism.closeDown(true);
  		} catch (PrismException e) {
  			System.err.println("Error: " + e.getMessage());
  		} catch (FileNotFoundException e) {
  			System.err.println("Error: " + e.getMessage());
  		}
  
  	}
  }
  