# Checking Jumping Frogs
## Simulating Frogs
“`
spin frogs.pml
“`
If you want all outputs left-aligned, use:
“`
spin -T frogs.pml
“`
## Verifying Frogs
### “Default” Verification
“`
spin -run frogs.pml
“`
Always finds one of deadlocking states.
### Displaying/Re-playing the “trail”
“`
spin -t frogs.pml
“`
Again, you can add the option `-T` to align the output.
### Ignoring Deadlock
“`
spin -run -E frogs.pml
“`
However, if we run this with a simple correct model, we find no errors.
The only “default” errors in the frog model are deadlocks.
## Finding a Solution
Simulation is very unlikely to show a correct solution. Default verification can only find the deadlocks. How do we use the model to generate a possible solution?
### Hint
Consider some assertion `done` that would be true if and only if the frogs had managed
to change places as required. Add the line `assert(!done)` at end of the model.
Then a deadlock-ignoring verification run will find a solution because:
it does an exhaustive search of all possible executions,
so it will find the sequence that leads to `done` actually being true,
leading to the line `assert(!done)` to signal a verification error.
The trail file will contain the sequence that lead to `done` being true,
making that assertion fail. Replaying that trail file gives a solution.
| No | Answer |
| —- | ————————– |
| 12 | true |
| 13 | false |
| 14 | false ? |
| 15 | false |
| 16 | true |
| 17 | true ? |
| 18 | false |
| 19 | false |
| 20 | true |
| 21 | true |
| 22 | B |
| 23 | D |
| 24 | B |
| 25 | D |
| 26 | A |
| 27 | A |
| 28 | C |
| 29 | D |
| 30 | C ? |
| 31 | B |
T(n) = 3 T(n/2) + n
T(n) = 8 T(n/4) + n^1.5
T(n) = 4 T(n/2) + nlog(n)
T(n) = 5 T(n/3) + nlog(n)
mk^2 / mk
= k