CS计算机代考程序代写 # Checking Jumping Frogs

# 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