Examples - Modest Toolset

The Modest Toolset download contains a Samples folder with a number of example models and case studies that can be analysed with the various tools:

Probabilistic Models

beb.modest:
Modest MDP model of a bounded exponential backoff procedure (BEB) [BFHH11].
Parameters: K (maximum value of backoff counter), N (number of tries before giving up) and H (number of hosts).
Can be model-checked with mcsta and simulated with modes (using uniform resolution of structural nondeterminism).
die.jani:
JANI DTMC model of Knuth's algorithm to simulate a die using only fair coins.
Can be model-checked with mcsta and simulated with modes.
dining-cryptographers-*.modest:
Modest MDP model of the randomised dining cryptographers PRISM case study.
Parameters: * (number of cryptographers).
Can be model-checked with mcsta and simulated with modes (using uniform resolution of structural nondeterminism).
knuth-dice-sum.modest:
Modest MDP model of using Knuth's algorithm to simulate a die using only fair coins for two dice.
Can be model-checked with mcsta and simulated with modes (using uniform resolution of structural nondeterminism).
knuth-die.modest:
Modest DTMC model of Knuth's algorithm to simulate a die using only fair coins.
Can be model-checked with mcsta and simulated with modes.

brp.modest:
Modest PTA model of the bounded retransmission protocol (BRP) [HH09].
Parameters: N (number of frames per file), MAX (maximum number of retransmissions per frame) and TD (transmission delay).
Can be model-checked with mcsta and simulated with modes (using as-soon/late-as-possible resolution of temporal nondeterminism).
csmacd.modest:
Modest PTA model for the IEEE 802.3 CSMA/CD protocol [HH09].
Parameters: RED (time reduction factor), BCMAX (maximum value of backoff counter).
Can be model-checked with mcsta and simulated with modes (using uniform resolution of structural nondeterminism and as-soon/late-as-possible resolution of temporal nondeterminism).
mpeg4-reduced.xsadf:
XSADF PTA model of the MPEG-4 example, reduced version [HHB16].
Can be model-checked with mcsta and simulated with modes (using uniform resolution of structural nondeterminism).
wlan.modest:
Modest PTA model of IEEE 802.11 Wireless LAN [HH09].
Parameters: BCMAX (maximum value of backoff counter).
Can be model-checked with mcsta and simulated with modes (using uniform resolution of structural nondeterminism and as-soon/late-as-possible resolution of temporal nondeterminism).

fileserver.modest:
Modest STA model of a file server with exponentially distributed arrivals, uniformly distributed file size, fixed probability for file to be in archive, and nondeterministic time for archive retrieval [HHH14].
Parameters: TIME_BOUND (property time bound).
Can be model-checked with mcsta and simulated with modes (using uniform resolution of structural nondeterminism and as-soon/late-as-possible resolution of temporal nondeterminism).
m-g-1-c-queue.modest:
Modest STA model of a fixed-capacity queue with exponentially distributed arrivals, normally distributed service time [HHH14].
Parameters: TIME_BOUND (property time bound).
Can be model-checked with mcsta and simulated with modes (using as-soon/late-as-possible resolution of temporal nondeterminism).
tandem-queue.modest:
Modest STA model of the tandem queueing benchmark [HHH14].
Parameters: SCALE (time scaling factor), TIME_BOUND (property time bound).
Can be model-checked with mcsta and simulated with modes (using uniform resolution of structural nondeterminism and as-soon/late-as-possible resolution of temporal nondeterminism).

etcs.modest:
Modest SHA model of moving block train control as used in ETCS level 3 [HHHK13].
Parameters: SIGMA (standard deviation of position measurements), TIME_BOUND (property time bound).
Can be model-checked with prohver.
thermostat.modest:
Modest PHA model of a thermostat with failure [HHHK13].
Parameters: TIME_BOUND (property time bound).
Can be model-checked with prohver.
waterlevel.modest:
Modest SHA model of a water level control system [HHHK13].
Parameters: TIME_BOUND (property time bound).
Can be model-checked with prohver.