example of TLA+ based solution to the problem from Die Hard Movie ( inspired by Leslie Lamport's tutorial)

the 'invariant' BigNot4 defined in config file is violated and Model checker shows the steps ( = sequence of states = behavior) leading up to it thus solving for us the problem of filling exactly 4 gallons into big bucket