> Given a dtmc model, which is an instance of ProbModel class, how can I
> find all paths and also traces of a single variable symbolically?
Could you clarify a bit what you concretely want to do? Do you want to
check something for these paths (symbolically) or do you want to output
the paths? Something like "from the initial state, for each reachable
state give me a path that shows that it can be reached?"
There is functionality in the symbolic CTL model checker of PRISM to
generate counter-examples/witnesses: E.g., for
E[ F "goal" ]
you will get a witness that demonstrates that one state satisfying
"goal" can be reached from an initial state.
-pf 'E[ F s=7 ]'
Result: true (property satisfied in the initial state)
This is implemented in prism.NonProbModelChecker in the method
checkExistsUntil. The general idea is to perform a symbolic reachability
computation and to store in each iteration step the set of newly
discovered states. Then, once a target state has been reached, one can
trace back through these sets to construct a path to one of the initial
Depending on what you want to achieve, this might give you some ideas.