Tracking QComp Model Support
Properties
DTMC
P, Pb
MDP
P, Pb
Models
Note: Models listed below are those which contain at least one supported property. Each MODELNAME
is associated with a tuple (MODELFILE
, PROPERTYFILE
). The model may be found at data/models/MODELFILE
and the property at data/properties/PROPERTYFILE
. Additionally, constants which are used for QComp may be found at data/consts/MODELNAME.consts
.
DTMC
Jani models (unsupported)
Prism models
- crowds - (crowds.prism, crowds.props)
- egl - (egl.prism, egl.props)
- haddad-monmege - (haddad-monmege.pm, haddad-monmege.prctl)
MDP
Jani Models (unsupported)
Prism Models
- consensus - (consensus.4.prism, consensus.props), (consensus.6.prism, consensus.props)
- csma - (csma.3-4.prism, csma.props), (csma.4-2.prism, csma.props)
- firewire - (firewire.false.prism, firewire.false.props)
- pacman - (pacman.nm, pacman.props)
- pnueli-zuck - (pnueli-zuck.5.prism, pnueli-zuck.props), (pnueli-zuck.10.prism, pnueli-zuck.props)
- rabin - (rabin.10.prism, rabin.10.props)
- resource-gathering - (resource-gathering.pm, resource-gathering.prctl)
- wlan - (wlan.4.prism, wlan.props), (wlan.5.prism, wlan.props), (wlan.6.prism, wlan.props)
- zeroconf - (zeroconf.prism, zeroconf.props)