org.eclipse.emf.henshin.statespace.external.prism
Class PRISMUtil

java.lang.Object
  org.eclipse.emf.henshin.statespace.external.prism.PRISMUtil

public class PRISMUtil
extends Object

PRISM utils.

Nested Class Summary

static class

PRISMUtil.Range Data class for ranges (and constants).

Field Summary

static String	PRISM_ARGS_KEY
static String	PRISM_EXPERIMENT_KEY
static String	PRISM_PATH_KEY
static String	STATE_VARIABLE

Constructor Summary

PRISMUtil()

Method Summary

static String	expandLabels(String template, StateSpaceIndex index, org.eclipse.core.runtime.IProgressMonitor monitor)
static Map<String,String>	getAllProbs(StateSpace stateSpace, boolean force) Get all probabilities for a state space.
static Map<String,String>	getAllRates(StateSpace stateSpace, boolean force) Get all rates for a state space.
static String	getConstants(StateSpace stateSpace)
static String	getModelHeader(String modelType)
static String	getPRISMArgs(StateSpace stateSpace) Get the PRISM arguments property.
static String	getPRISMExperiment(StateSpace stateSpace) Get the PRISM experiment parameter.
static File	getPRISMPath(StateSpace stateSpace) Get the PRISM path property.
static String	getPRISMState(int index, String extra, boolean successor)
static String	getPRISMStates(List<State> states)
static String	getProb(StateSpace stateSpace, Rule rule, int index) Get the probability of a rule, as specified in the state space properties.
static Map<String,List<Rule>>	getProbabilisticRules(StateSpace stateSpace) Partition the rules of a state space into probabilistic rules, based on their names.
static PRISMUtil.Range	getProbAsRange(StateSpace stateSpace, Rule rule, int index) Get the probability of a rule, as specified in the state space properties.
static String	getProbKey(Rule rule, int index) Get the properties key for rule probabilities.
static String	getProbVar(int index) Get the variable name for a rule probability.
static String	getRate(StateSpace stateSpace, Rule rule) Get the rate of a rule, as specified in the state space properties.
static PRISMUtil.Range	getRateAsRange(StateSpace stateSpace, Rule rule) Get the rate of a rule, as specified in the state space properties.
static String	getRateKey(Rule rule) Get the properties key for rule rates.
static String	getVariableDeclarations(int size, boolean explicit)
protected static Process	invokePRISM(StateSpace stateSpace, File modelFile, File formulaFile, String[] args, Map<String,String> constants, boolean allowExperiments, org.eclipse.core.runtime.IProgressMonitor monitor) Invoke PRISM on a state space.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

STATE_VARIABLE

public static final String STATE_VARIABLE

See Also:

Constant Field Values

PRISM_PATH_KEY

public static final String PRISM_PATH_KEY

See Also:

Constant Field Values

PRISM_ARGS_KEY

public static final String PRISM_ARGS_KEY

See Also:

Constant Field Values

PRISM_EXPERIMENT_KEY

public static final String PRISM_EXPERIMENT_KEY

See Also:

Constant Field Values

Constructor Detail

PRISMUtil

public PRISMUtil()

Method Detail

invokePRISM

protected static Process invokePRISM(StateSpace stateSpace,
                                     File modelFile,
                                     File formulaFile,
                                     String[] args,
                                     Map<String,String> constants,
                                     boolean allowExperiments,
                                     org.eclipse.core.runtime.IProgressMonitor monitor)
                              throws Exception

Invoke PRISM on a state space.

Parameters:

stateSpace - State space.

args - Arguments.

monitor - Monitor.

Returns:

Created process.

Throws:

Exception - On errors.

expandLabels

public static String expandLabels(String template,
                                  StateSpaceIndex index,
                                  org.eclipse.core.runtime.IProgressMonitor monitor)
                           throws Exception

Throws:

Exception

getRateKey

public static String getRateKey(Rule rule)

Get the properties key for rule rates.

getRate

public static String getRate(StateSpace stateSpace,
                             Rule rule)

Get the rate of a rule, as specified in the state space properties.

getRateAsRange

public static PRISMUtil.Range getRateAsRange(StateSpace stateSpace,
                                             Rule rule)
                                      throws ParseException

Get the rate of a rule, as specified in the state space properties.

Throws:

ParseException

getAllRates

public static Map<String,String> getAllRates(StateSpace stateSpace,
                                             boolean force)

Get all rates for a state space.

Parameters:

stateSpace - The state space.

force - Whether the rate must be specified.

Returns:

Map associating constants to values.

getProbKey

public static String getProbKey(Rule rule,
                                int index)

Get the properties key for rule probabilities.

getProbVar

public static String getProbVar(int index)

Get the variable name for a rule probability.

getProb

public static String getProb(StateSpace stateSpace,
                             Rule rule,
                             int index)

Get the probability of a rule, as specified in the state space properties.

getProbAsRange

public static PRISMUtil.Range getProbAsRange(StateSpace stateSpace,
                                             Rule rule,
                                             int index)
                                      throws ParseException

Get the probability of a rule, as specified in the state space properties.

Throws:

ParseException

getAllProbs

public static Map<String,String> getAllProbs(StateSpace stateSpace,
                                             boolean force)

Get all probabilities for a state space.

Parameters:

stateSpace - The state space.

force - Whether the probability must be specified.

Returns:

Map associating constants to values.

getProbabilisticRules

public static Map<String,List<Rule>> getProbabilisticRules(StateSpace stateSpace)

Partition the rules of a state space into probabilistic rules, based on their names. That is, all rules with the same name become part of one probabilistic rule. The derived probabilistic rules are meaningful in the context of an MDP.

Parameters:

stateSpace - State space.

Returns:

Probabilistic rules.

getConstants

public static String getConstants(StateSpace stateSpace)

getPRISMPath

public static File getPRISMPath(StateSpace stateSpace)

Get the PRISM path property.

Parameters:

stateSpace - State space.

Returns:

PRISM path property (can be null)

getPRISMArgs

public static String getPRISMArgs(StateSpace stateSpace)

Get the PRISM arguments property.

Parameters:

stateSpace - State space.

Returns:

PRISM arguments property (can be null)

getPRISMExperiment

public static String getPRISMExperiment(StateSpace stateSpace)

Get the PRISM experiment parameter.

Parameters:

stateSpace - State space.

Returns:

PRISM experiment parameter (can be null)

getVariableDeclarations

public static String getVariableDeclarations(int size,
                                             boolean explicit)

getModelHeader

public static String getModelHeader(String modelType)

getPRISMState

public static String getPRISMState(int index,
                                   String extra,
                                   boolean successor)

getPRISMStates

public static String getPRISMStates(List<State> states)