Browse Source
Remove ModelExplorer interface and replace with ModelGenerator.
Remove ModelExplorer interface and replace with ModelGenerator.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10992 bbc10eb1-c90d-0410-af57-cb519fbb1720master
Dave Parker
10 years ago
5 changed files with 56 additions and 276 deletions
-
81prism/src/explicit/FastAdaptiveUniformisation.java
-
16prism/src/explicit/FastAdaptiveUniformisationModelChecker.java
-
99prism/src/explicit/ModelExplorer.java
-
11prism/src/prism/Prism.java
-
125prism/src/simulator/PrismModelExplorer.java
@ -1,99 +0,0 @@ |
|||
//============================================================================== |
|||
// |
|||
// Authors: |
|||
// * Dave Parker <david.parker@comlab.ox.ac.uk> (University of 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 explicit; |
|||
|
|||
import parser.State; |
|||
import prism.PrismException; |
|||
|
|||
public interface ModelExplorer |
|||
{ |
|||
public State getDefaultInitialState() throws PrismException; |
|||
|
|||
public void queryState(State state) throws PrismException; |
|||
|
|||
public void queryState(State state, double time) throws PrismException; |
|||
|
|||
/** |
|||
* Returns the current number of available choices. |
|||
* @throws PrismException |
|||
*/ |
|||
public int getNumChoices() throws PrismException; |
|||
|
|||
/** |
|||
* Returns the current (total) number of available transitions. |
|||
* @throws PrismException |
|||
*/ |
|||
public int getNumTransitions() throws PrismException; |
|||
|
|||
/** |
|||
* Returns the current number of available transitions in choice i. |
|||
* @throws PrismException |
|||
*/ |
|||
public int getNumTransitions(int i) throws PrismException; |
|||
|
|||
/** |
|||
* Get the probability/rate of a transition within a choice, specified by its index/offset. |
|||
*/ |
|||
public double getTransitionProbability(int i, int offset) throws PrismException; |
|||
|
|||
/** |
|||
* Get the action label of a transition as a string, specified by its index/offset. |
|||
* (null for asynchronous/independent transitions) |
|||
* (see also {@link #getTransitionModuleOrAction(int, int)} and {@link #getTransitionModuleOrActionIndex(int, int)}) |
|||
* TODO: change return type to Object? |
|||
* @throws PrismException |
|||
*/ |
|||
public String getTransitionAction(int i, int offset) throws PrismException; |
|||
|
|||
/** |
|||
* Get the action label of a transition as a string, specified by its index. |
|||
* (null for asynchronous/independent transitions) |
|||
* (see also {@link #getTransitionModuleOrAction(int)} and {@link #getTransitionModuleOrActionIndex(int)}) |
|||
* TODO: change return type to Object? |
|||
* @throws PrismException |
|||
*/ |
|||
public String getTransitionAction(int index) throws PrismException; |
|||
|
|||
/** |
|||
* Get the probability/rate of a transition, specified by its index. |
|||
*/ |
|||
public double getTransitionProbability(int i) throws PrismException; |
|||
|
|||
/** |
|||
* Get the sum of probabilities/rates for transitions. |
|||
*/ |
|||
// public double getTransitionProbabilitySum() throws PrismException; |
|||
|
|||
/** |
|||
* Get the target (as a new State object) of a transition within a choice, specified by its index/offset. |
|||
*/ |
|||
public State computeTransitionTarget(int i, int offset) throws PrismException; |
|||
|
|||
/** |
|||
* Get the target of a transition (as a new State object), specified by its index. |
|||
*/ |
|||
public State computeTransitionTarget(int i) throws PrismException; |
|||
} |
|||
@ -1,125 +0,0 @@ |
|||
//============================================================================== |
|||
// |
|||
// Authors: |
|||
// * Dave Parker <david.parker@comlab.ox.ac.uk> (University of 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 simulator; |
|||
|
|||
import parser.State; |
|||
import parser.ast.ModulesFile; |
|||
import prism.PrismException; |
|||
import explicit.ModelExplorer; |
|||
|
|||
public class PrismModelExplorer implements ModelExplorer |
|||
{ |
|||
private SimulatorEngine simEngine; |
|||
private ModulesFile modulesFile; |
|||
|
|||
public PrismModelExplorer(SimulatorEngine simEngine, ModulesFile modulesFile) throws PrismException |
|||
{ |
|||
this.simEngine = simEngine; |
|||
this.modulesFile = modulesFile; |
|||
simEngine.createNewOnTheFlyPath(modulesFile); |
|||
|
|||
} |
|||
|
|||
@Override |
|||
public State getDefaultInitialState() throws PrismException |
|||
{ |
|||
return modulesFile.getDefaultInitialState(); |
|||
} |
|||
|
|||
@Override |
|||
public void queryState(State state) throws PrismException |
|||
{ |
|||
simEngine.initialisePath(state); |
|||
} |
|||
|
|||
@Override |
|||
public void queryState(State state, double time) throws PrismException |
|||
{ |
|||
queryState(state); |
|||
} |
|||
|
|||
@Override |
|||
public int getNumChoices() throws PrismException |
|||
{ |
|||
return simEngine.getNumChoices(); |
|||
} |
|||
|
|||
@Override |
|||
public int getNumTransitions() throws PrismException |
|||
{ |
|||
return simEngine.getNumTransitions(); |
|||
} |
|||
|
|||
@Override |
|||
public int getNumTransitions(int i) throws PrismException |
|||
{ |
|||
return simEngine.getNumTransitions(i); |
|||
} |
|||
|
|||
@Override |
|||
public String getTransitionAction(int i, int offset) throws PrismException |
|||
{ |
|||
return simEngine.getTransitionAction(i, offset); |
|||
} |
|||
|
|||
@Override |
|||
public String getTransitionAction(int i) throws PrismException |
|||
{ |
|||
return simEngine.getTransitionAction(i); |
|||
} |
|||
|
|||
@Override |
|||
public double getTransitionProbability(int i, int offset) throws PrismException |
|||
{ |
|||
return simEngine.getTransitionProbability(i, offset); |
|||
} |
|||
|
|||
@Override |
|||
public double getTransitionProbability(int i) throws PrismException |
|||
{ |
|||
return simEngine.getTransitionProbability(i); |
|||
} |
|||
|
|||
/* |
|||
@Override |
|||
public double getTransitionProbabilitySum() throws PrismException |
|||
{ |
|||
return simEngine.getTransitionProbabilitySum(); |
|||
} |
|||
*/ |
|||
|
|||
@Override |
|||
public State computeTransitionTarget(int i, int offset) throws PrismException |
|||
{ |
|||
return simEngine.computeTransitionTarget(i, offset); |
|||
} |
|||
|
|||
@Override |
|||
public State computeTransitionTarget(int i) throws PrismException |
|||
{ |
|||
return simEngine.computeTransitionTarget(i); |
|||
} |
|||
} |
|||
Write
Preview
Loading…
Cancel
Save
Reference in new issue