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 modelchecked 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 modelchecked with mcsta and simulated with modes.

diningcryptographers*.modest:
Modest MDP model of the randomised dining cryptographers PRISM case study.
Parameters: * (number of cryptographers).
Can be modelchecked with mcsta and simulated with modes (using uniform resolution of structural nondeterminism).

knuthdicesum.modest:
Modest MDP model of using Knuth's algorithm to simulate a die using only fair coins for two dice.
Can be modelchecked with mcsta and simulated with modes (using uniform resolution of structural nondeterminism).

knuthdie.modest:
Modest DTMC model of Knuth's algorithm to simulate a die using only fair coins.
Can be modelchecked with mcsta and simulated with modes.
Probabilistic Timed Models

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 modelchecked with mcsta and simulated with modes (using assoon/lateaspossible 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 modelchecked with mcsta and simulated with modes (using uniform resolution of structural nondeterminism and assoon/lateaspossible resolution of temporal nondeterminism).

mpeg4reduced.xsadf:
XSADF PTA model of the MPEG4 example, reduced version [HHB16].
Can be modelchecked 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 modelchecked with mcsta and simulated with modes (using uniform resolution of structural nondeterminism and assoon/lateaspossible resolution of temporal nondeterminism).
Stochastic Timed Models

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 modelchecked with mcsta and simulated with modes (using uniform resolution of structural nondeterminism and assoon/lateaspossible resolution of temporal nondeterminism).

mg1cqueue.modest:
Modest STA model of a fixedcapacity queue with exponentially distributed arrivals, normally distributed service time [HHH14].
Parameters: TIME_BOUND (property time bound).
Can be modelchecked with mcsta and simulated with modes (using assoon/lateaspossible resolution of temporal nondeterminism).

tandemqueue.modest:
Modest STA model of the tandem queueing benchmark [HHH14].
Parameters: SCALE (time scaling factor), TIME_BOUND (property time bound).
Can be modelchecked with mcsta and simulated with modes (using uniform resolution of structural nondeterminism and assoon/lateaspossible resolution of temporal nondeterminism).
Hybrid Models

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 modelchecked with prohver.

thermostat.modest:
Modest PHA model of a thermostat with failure [HHHK13].
Parameters: TIME_BOUND (property time bound).
Can be modelchecked with prohver.

waterlevel.modest:
Modest SHA model of a water level control system [HHHK13].
Parameters: TIME_BOUND (property time bound).
Can be modelchecked with prohver.