Alloy 6 German Wikipedia Uhr Example -- question on run command

Questions
1

When I run the Alloy 6 wikipedia clock example with alloy 6.1

one sig Uhr {
	var stunde: one Int
}
pred init {
	Uhr.stunde = 1
}
pred move {
	Uhr.stunde = 12 implies Uhr.stunde' = 1 else Uhr.stunde' = Uhr.stunde.plus[1]
}
fact trans {
	init
	always move
}
run {} for 5 int, 12 steps

which steps through 12 steps, perfect
(0) → (1) → (2) → … → (11) ----> back to (0)

when I just do

run{}

and step though it manually I see just
(0) → (0) → … → continuous with (0)

Is there any way to avoid to set the steps manually in run. I would assume this should be part of the model? why is for 5 int necessary as well?
As I am just doing the first steps in allow 6, so maybe the answer is trivial.

2

Back from vacation…

I can’t reproduce this. I rather get a “no instance found” message. Are you sure you copy-pasted the exact same model?

If you don’t specify the number of steps in a command, there is a default of 10. But you need at least 12 different states to go from 1 to 12, so 12 steps is a minimum that must be specified explicitly.

Furthermore, for performance reasons, integers have a special status in Alloy: if you write for N int (for some N), you get integers exactly in -2^(N-1) .. 2^(N-1) - 1, as integers in most programming languages. So, if you want Uhr.stunde to reach 12, you need N >= 5.

All in all, this example is perhaps not that well suited to beginners as it depends on the peculiar way Alloy handles integers. It’s also not very representative of the strength and applicability of Alloy.