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

**URL:** https://alloytools.discourse.group/t/alloy-6-german-wikipedia-uhr-example-question-on-run-command/477
**Category:** Questions
**Created:** [August 10, 2024, 3:37pm UTC](https://alloytools.discourse.group/t/alloy-6-german-wikipedia-uhr-example-question-on-run-command/477 "2024-08-10T15:37:54Z")
**Posts on this page:** 2
**Page:** 1

<div class="post-metadata">

### Author: ![WolfgangSpahn](https://avatars.discourse-cdn.com/v4/letter/w/c0e974/32.png) [@WolfgangSpahn](https://alloytools.discourse.group/u/WolfgangSpahn)
#### Post date: [August 10, 2024, 3:37pm UTC](https://alloytools.discourse.group/t/alloy-6-german-wikipedia-uhr-example-question-on-run-command/477/1 "2024-08-10T15:37:54Z")

</div>

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

```auto
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

```auto
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.

---

<div class="post-metadata">

### Author: ![grayswandyr](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/grayswandyr/32/17_2.png) [@grayswandyr](https://alloytools.discourse.group/u/grayswandyr)
#### Post date: [August 26, 2024, 7:20am UTC](https://alloytools.discourse.group/t/alloy-6-german-wikipedia-uhr-example-question-on-run-command/477/2 "2024-08-26T07:20:10Z")

</div>

Back from vacation…

> [@WolfgangSpahn](#):
>
> when I just do
> 
> ```auto
> run{}
> 
> ```
> 
> and step though it manually I see just  
> (0) → (0) → … → continuous with (0)

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

> [@WolfgangSpahn](#):
>
> 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.

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.
