Browse Source

explicit.DTMC/MDP: provide forEachTransition and sumOverTransitions methods

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12092 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Joachim Klein 9 years ago
parent
commit
f669ac11d9
  1. 72
      prism/src/explicit/DTMC.java
  2. 72
      prism/src/explicit/MDP.java

72
prism/src/explicit/DTMC.java

@ -54,6 +54,78 @@ public interface DTMC extends Model
*/
public Iterator<Entry<Integer, Pair<Double, Object>>> getTransitionsAndActionsIterator(int s);
/**
* Functional interface for a consumer,
* accepting transitions (s,t,d), i.e.,
* from state s to state t with value d.
*/
@FunctionalInterface
public interface TransitionConsumer {
void accept(int s, int t, double d);
}
/**
* Iterate over the outgoing transitions of state {@code s} and call the accept method
* of the consumer for each of them:
* <br>
* Call {@code accept(s,t,d)} where t is the successor state and,
* in a DTMC, d = P(s,t) is the probability from s to t,
* while in CTMC, d = R(s,t) is the rate from s to t.
* <p>
* <i>Default implementation</i>: The default implementation relies on iterating over the
* iterator returned by {@code getTransitionsIterator()}.
* <p><i>Note</i>: This method is the base for the default implementation of the numerical
* computation methods (mvMult, etc). In derived classes, it may thus be worthwhile to
* provide a specialised implementation for this method that avoids using the Iterator mechanism.
*
* @param s the state s
* @param c the consumer
*/
public default void forEachTransition(int s, TransitionConsumer c)
{
for (Iterator<Entry<Integer, Double>> it = getTransitionsIterator(s); it.hasNext(); ) {
Entry<Integer, Double> e = it.next();
c.accept(s, e.getKey(), e.getValue());
}
}
/**
* Functional interface for a function
* mapping transitions (s,t,d), i.e.,
* from state s to state t with value d
* to a double value.
*/
@FunctionalInterface
public interface TransitionToDoubleFunction {
double apply(int s, int t, double d);
}
/**
* Iterate over the outgoing transitions of state {@code s}, call the function {@code f}
* and return the sum of the result values:
* <br>
* Return sum_t f(s, t, P(s,t)), where t ranges over the successors of s.
*
* @param s the state s
* @param c the consumer
*/
public default double sumOverTransitions(final int s, final TransitionToDoubleFunction f)
{
class Sum {
double sum = 0.0;
void accept(int s, int t, double d)
{
sum += f.apply(s, t, d);
}
}
Sum sum = new Sum();
forEachTransition(s, sum::accept);
return sum.sum;
}
/**
* Perform a single step of precomputation algorithm Prob0 for a single state,
* i.e., for the state {@code s} returns true iff there is a transition from

72
prism/src/explicit/MDP.java

@ -46,6 +46,78 @@ public interface MDP extends NondetModel
*/
public Iterator<Entry<Integer, Double>> getTransitionsIterator(int s, int i);
/**
* Functional interface for a consumer,
* accepting transitions (s,t,d), i.e.,
* from state s to state t with value d.
*/
@FunctionalInterface
public interface TransitionConsumer {
void accept(int s, int t, double d);
}
/**
* Iterate over the outgoing transitions of state {@code s} and choice {@code i}
* and call the accept method of the consumer for each of them:
* <br>
* Call {@code accept(s,t,d)} where t is the successor state d = P(s,i,t)
* is the probability from s to t with choice i.
* <p>
* <i>Default implementation</i>: The default implementation relies on iterating over the
* iterator returned by {@code getTransitionsIterator()}.
* <p><i>Note</i>: This method is the base for the default implementation of the numerical
* computation methods (mvMult, etc). In derived classes, it may thus be worthwhile to
* provide a specialised implementation for this method that avoids using the Iterator mechanism.
*
* @param s the state s
* @param i the choice i
* @param c the consumer
*/
public default void forEachTransition(int s, int i, TransitionConsumer c)
{
for (Iterator<Entry<Integer, Double>> it = getTransitionsIterator(s, i); it.hasNext(); ) {
Entry<Integer, Double> e = it.next();
c.accept(s, e.getKey(), e.getValue());
}
}
/**
* Functional interface for a function
* mapping transitions (s,t,d), i.e.,
* from state s to state t with value d,
* to a double value.
*/
@FunctionalInterface
public interface TransitionToDoubleFunction {
double apply(int s, int t, double d);
}
/**
* Iterate over the outgoing transitions of state {@code s} and choice {@code i},
* call the function {@code f} and return the sum of the result values:
* <br>
* Return sum_t f(s, t, P(s,i,t)), where t ranges over the i-successors of s.
*
* @param s the state s
* @param c the consumer
*/
public default double sumOverTransitions(final int s, final int i, final TransitionToDoubleFunction f)
{
class Sum {
double sum = 0.0;
void accept(int s, int t, double d)
{
sum += f.apply(s, t, d);
}
}
Sum sum = new Sum();
forEachTransition(s, i, sum::accept);
return sum.sum;
}
/**
* Perform a single step of precomputation algorithm Prob0, i.e., for states i in {@code subset},
* set bit i of {@code result} iff, for all/some choices,

Loading…
Cancel
Save