diff --git a/prism/src/parser/ast/ModulesFile.java b/prism/src/parser/ast/ModulesFile.java index 842933cf..4131ccc7 100644 --- a/prism/src/parser/ast/ModulesFile.java +++ b/prism/src/parser/ast/ModulesFile.java @@ -352,11 +352,22 @@ public class ModulesFile extends ASTElement return moduleNames; } + /** + * Get the list of action names. + */ public Vector getSynchs() { return synchs; } + /** + * Get the {@code i}th action name (0-indexed). + */ + public String getSynch(int i) + { + return synchs.get(i); + } + public boolean isSynch(String s) { if (synchs == null) diff --git a/prism/src/simulator/Choice.java b/prism/src/simulator/Choice.java index 44f7c777..57736804 100644 --- a/prism/src/simulator/Choice.java +++ b/prism/src/simulator/Choice.java @@ -31,20 +31,71 @@ import prism.*; public interface Choice { -// public void setAction(String action); + /** + * Get the module/action for this choice, as an integer index + * (-i for independent in ith module, i for synchronous on ith action) + * (in both cases, modules/actions are 1-indexed) + */ public int getModuleOrActionIndex(); + + /** + * Get the module/action for this choice, as a string + * (form is "module" or "[action]") + */ public String getModuleOrAction(); + + /** + * Get the number of transitions in this choice. + */ public int size(); - public double getProbability(); - public double getProbability(int i); - public double getProbabilitySum(); + + /** + * Get the updates of the ith transition, as a string. + * This is in abbreviated form, i.e. x'=1, rather than x'=x+1. + * Format is: x'=1, y'=0, with empty string for empty update. + * Only variables updated are included in list (even if unchanged). + */ public String getUpdateString(int i, State currentState) throws PrismLangException; + + /** + * Get the updates of the ith transition, as a string. + * This is in full, i.e. of the form x'=x+1, rather than x'=1. + * Format is: (x'=x+1) & (y'=y-1), with empty string for empty update. + * Only variables updated are included in list. + * Note that expressions may have been simplified from original model. + */ public String getUpdateStringFull(int i); - public State computeTarget(State currentState) throws PrismLangException; - public void computeTarget(State currentState, State newState) throws PrismLangException; + + /** + * Compute the target for the ith transition, based on a current state, + * returning the result as a new State object copied from the existing one. + */ public State computeTarget(int i, State currentState) throws PrismLangException; + + /** + * Compute the target for the ith transition, based on a current state. + * Apply changes in variables to a provided copy of the State object. + * (i.e. currentState and newState should be equal when passed in.) + */ public void computeTarget(int i, State currentState, State newState) throws PrismLangException; + + /** + * Get the probability/rate for the ith transition. + */ + public double getProbability(int i); + + /** + * Get the sum of probabilities/rates for all transitions. + */ + public double getProbabilitySum(); + + /** + * Return the index of a transition according to a probability (or rate) sum, x. + * i.e. return the index of the first transition in this choice for which the + * sum of probabilities/rates for that and all prior transitions exceeds x. + */ public int getIndexByProbabilitySum(double x); + public void checkValid(ModelType modelType) throws PrismException; /** diff --git a/prism/src/simulator/ChoiceListFlexi.java b/prism/src/simulator/ChoiceListFlexi.java index 2aa4ced2..a8175fbb 100644 --- a/prism/src/simulator/ChoiceListFlexi.java +++ b/prism/src/simulator/ChoiceListFlexi.java @@ -153,20 +153,13 @@ public class ChoiceListFlexi implements Choice // Get methods - /** - * Get the module/action for this choice, as an integer index - * (-i for independent in ith module, i for synchronous on ith action) - * (in both cases, modules/actions are 1-indexed) - */ + @Override public int getModuleOrActionIndex() { return moduleOrActionIndex; } - /** - * Get the module/action for this choice, as a string - * (form is "module" or "[action]") - */ + @Override public String getModuleOrAction() { // Action label (or absence of) will be the same for all updates in a choice @@ -178,20 +171,13 @@ public class ChoiceListFlexi implements Choice return "[" + c.getSynch() + "]"; } - /** - * Get the number of transitions in this choice. - */ + @Override public int size() { return probability.size(); } - /** - * Get the updates of the ith transition, as a string. - * This is in abbreviated form, i.e. x'=1, rather than x'=x+1. - * Format is: x'=1, y'=0, with empty string for empty update. - * Only variables updated are included in list (even if unchanged). - */ + @Override public String getUpdateString(int i, State currentState) throws PrismLangException { int j, n; @@ -210,13 +196,7 @@ public class ChoiceListFlexi implements Choice return s; } - /** - * Get the updates of the ith transition, as a string. - * This is in full, i.e. of the form x'=x+1, rather than x'=1. - * Format is: (x'=x+1) & (y'=y-1), with empty string for empty update. - * Only variables updated are included in list. - * Note that expressions may have been simplified from original model. - */ + @Override public String getUpdateStringFull(int i) { String s = ""; @@ -233,11 +213,7 @@ public class ChoiceListFlexi implements Choice return s; } - /** - * Compute the target for the ith transition, based on a current state, - * returning the result as a new State object copied from the existing one. - * NB: for efficiency, there are no bounds checks done on i. - */ + @Override public State computeTarget(int i, State currentState) throws PrismLangException { State newState = new State(currentState); @@ -246,42 +222,20 @@ public class ChoiceListFlexi implements Choice return newState; } - /** - * Compute the target for the ith transition, based on a current state. - * Apply changes in variables to a provided copy of the State object. - * (i.e. currentState and newState should be equal when passed in.) - * NB: for efficiency, there are no bounds checks done on i. - */ + @Override public void computeTarget(int i, State currentState, State newState) throws PrismLangException { for (Update up : updates.get(i)) up.update(currentState, newState); } - public State computeTarget(State currentState) throws PrismLangException - { - return computeTarget(0, currentState); - } - - public void computeTarget(State currentState, State newState) throws PrismLangException - { - computeTarget(0, currentState, newState); - } - - /** - * Get the probability rate for the ith transition. - * NB: for efficiency, there are no bounds checks done on i. - */ + @Override public double getProbability(int i) { return probability.get(i); } - public double getProbability() - { - return getProbability(0); - } - + @Override public double getProbabilitySum() { double sum = 0.0; @@ -290,11 +244,7 @@ public class ChoiceListFlexi implements Choice return sum; } - /** - * Return the index of a transition according to a probability (or rate) sum, x. - * i.e. return the index of the first transition in this choice for which the - * sum of probabilities/rates for that and all prior transitions exceeds x. - */ + @Override public int getIndexByProbabilitySum(double x) { int i, n; @@ -325,6 +275,7 @@ public class ChoiceListFlexi implements Choice } } + @Override public String toString() { int i, n; diff --git a/prism/src/simulator/SimulatorEngine.java b/prism/src/simulator/SimulatorEngine.java index b059c3c4..3760323a 100644 --- a/prism/src/simulator/SimulatorEngine.java +++ b/prism/src/simulator/SimulatorEngine.java @@ -807,8 +807,8 @@ public class SimulatorEngine } /** - * Get a string describing the action/module of a transition, specified by - * its index/offset. + * Get a string describing the action/module of a transition, specified by its index/offset. + * (form is "module" or "[action]") */ public String getTransitionModuleOrAction(int i, int offset) { @@ -817,12 +817,53 @@ public class SimulatorEngine /** * Get a string describing the action/module of a transition, specified by its index. + * (form is "module" or "[action]") */ public String getTransitionModuleOrAction(int index) { return transitionList.getTransitionModuleOrAction(index); } + /** + * Get the index of the action/module of a transition, specified by its index/offset. + * (-i for independent in ith module, i for synchronous on ith action) + * (in both cases, modules/actions are 1-indexed) + */ + public int getTransitionModuleOrActionIndex(int i, int offset) + { + return transitionList.getTransitionModuleOrActionIndex(transitionList.getTotalIndexOfTransition(i, offset)); + } + + /** + * Get the index of the action/module of a transition, specified by its index. + * (-i for independent in ith module, i for synchronous on ith action) + * (in both cases, modules/actions are 1-indexed) + */ + public int getTransitionModuleOrActionIndex(int index) + { + return transitionList.getTransitionModuleOrActionIndex(index); + } + + /** + * Get the action label of a transition as a string, specified by its index/offset. + * (null for asynchronous/independent transitions) + */ + public String getTransitionAction(int i, int offset) + { + int a = transitionList.getTransitionModuleOrActionIndex(transitionList.getTotalIndexOfTransition(i, offset)); + return a < 0 ? null : modulesFile.getSynch(a - 1); + } + + /** + * Get the action label of a transition as a string, specified by its index. + * (null for asynchronous/independent transitions) + */ + public String getTransitionAction(int index) + { + int a = transitionList.getTransitionModuleOrActionIndex(index); + return a < 0 ? null : modulesFile.getSynch(a - 1); + } + /** * Get the probability/rate of a transition within a choice, specified by its index/offset. */ diff --git a/prism/src/simulator/TransitionList.java b/prism/src/simulator/TransitionList.java index 080b9b68..68c0a671 100644 --- a/prism/src/simulator/TransitionList.java +++ b/prism/src/simulator/TransitionList.java @@ -179,12 +179,23 @@ public class TransitionList /** * Get a string describing the action/module of a transition, specified by its index. + * (form is "module" or "[action]") */ public String getTransitionModuleOrAction(int index) { return getChoiceOfTransition(index).getModuleOrAction(); } + /** + * Get the index of the action/module of a transition, specified by its index. + * (-i for independent in ith module, i for synchronous on ith action) + * (in both cases, modules/actions are 1-indexed) + */ + public int getTransitionModuleOrActionIndex(int index) + { + return getChoiceOfTransition(index).getModuleOrActionIndex(); + } + /** * Get the probability/rate of a transition, specified by its index. */