Probabilistic RED
A prototype tool for the reachability analysis of probabilistic timed automata based on an integrated quantitative state-space representation, which is an extension of RED diagrams.
cd redlib
make
cd ..
make
pta -Tg -Max -G0.000001 <.d> <.goal> <.prob>
pta -Tg -Min -G0.000001 <.d> <.goal> <.prob>
args | description |
---|---|
-Tg | reachability analysis |
-Max | maximum probability |
-Min | minimum probability |
-G | precision threshold |
<.d> | model file |
<.goal> | symbolic target state |
<.prob> | probability file |