modeling-at-night Modeling some problems in Alloy, nuXmv and TLA The Frog Puzzle (link) Alloy (here) TLA+ (here) nuXmv (here) Monopoly Alloy (exercise a) and (exercise b, c and d) Lights Out (link) nuXmv (here) some-other-exercises Alloy (here)