# Hello! Learning Alloy, can someone help me with a basic question on temporal models?

**URL:** <https://alloytools.discourse.group/t/hello-learning-alloy-can-someone-help-me-with-a-basic-question-on-temporal-models/288>\
**Category:** Questions\
**Created:** [September 27, 2022, 11:38pm UTC](https://alloytools.discourse.group/t/hello-learning-alloy-can-someone-help-me-with-a-basic-question-on-temporal-models/288 "2022-09-27T23:38:52Z")\
**Posts on this page:** 3\
**Page:** 1

<div class="post-metadata">

**Author:** ![roehst](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/roehst/32/156_2.png) [@roehst](https://alloytools.discourse.group/u/roehst)\
**Post date:** [September 27, 2022, 11:38pm UTC](https://alloytools.discourse.group/t/hello-learning-alloy-can-someone-help-me-with-a-basic-question-on-temporal-models/288/1 "2022-09-27T23:38:52Z")

</div>

This my first post, so **thanks** for the AMAZING tool that is Alloy. In our times, people sometimes feel entitled to the good stuff. But we know it takes a lot of effort. Alloy is an incredible contribution to the community!

I am trying to model a Virtual Machine with Services that are spawned, acquiring a PID.

I designed the `spawn` predicate to avoid two services being assigned the same PID.

Then I wrote `run` to `init`, run `spawn` a couple times and assert that two services share a PID.

But unfortunately I get examples, which means my model is not correct.

Could someone help with the basics?

1. Why can it find a model if the spawn predicate  
requires that a new pid is not used by any service?  
This should make for fresh pids.

2. Why there are conditions with more than  
one new pid? There is a framing condition to say  
that all other services remain the same…

3. Is this style of quantification correct the problem? I tried to avoid `one s : Service, p : Pid | spawn[s,p]` to make it more succint.

```auto
sig Service {
	var pid : lone Pid
}

sig Pid {}

pred spawn {

	one s : Service, p : Pid {

		no s.pid
	
		p not in Service.pid
	
		s.pid' = p
	
		(Service - s).pid' = (Service - s).pid

		p in Service.pid'

	}

}

fun online : set Pid {
	{ p : Pid | p in Service.pid }
}

pred init {
	no Service.pid
}

pred stutter {
	Service.pid' = Service.pid
}

pred sharing {
	some s : Service |
		some t : Service |
			s != t and s.pid = t.pid and some s.pid
}

run { 
	init
	and after spawn
	and after after spawn
	and after after after sharing
}

```

Help is much appreciated.

---

<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:** [September 28, 2022, 10:10am UTC](https://alloytools.discourse.group/t/hello-learning-alloy-can-someone-help-me-with-a-basic-question-on-temporal-models/288/2 "2022-09-28T10:10:43Z")

</div>

> [@roehst](#):
>
> There is a framing condition to say  
> that all other services remain the same…

Actually no: if you look at at states 2 and 3 of the trace, you’ll see that in both cases you indeed have `(Service - Service$1).pid' = (Service - Service$1).pid` (you can see this in going to state 2 and then use the Evaluator), while there was a change for `Service$2`.

This is because the frame condition is too lax: you don’t say that `pid` shouldn’t change for _each_ service (except `s`) but that `pid` shouldn’t change for the union of all services other than `s`. You could then rather write `all s2: Service - s | s2.pid' = s2.pid`.

> [@roehst](#):
>
> Is this style of quantification correct the problem? I tried to avoid `one s : Service, p : Pid | spawn[s,p]` to make it more succint.

In general, I see two issues with this sort of quantification:

1. `one` is a treacherous quantifier, because saying `one a:A, b: B| ...` is different than `one a:A | one b:B | ...`. `some`, `all` and `no` do not suffer from this source of confusion.
2. for events, you usually expect other stuff to be unchanged due to frame conditions, so the fact that there is exactly one pair of service and pid that changes should often be a property of your model rather than something you enforce.

All in all, I rewrote your model in what I think is a bit more idiomatic. Observe how `spawn` states that `pid` changes in `s->p` but remains otherwise the same.

```auto
sig Service {
	var pid : lone Pid
}

sig Pid {}

pred init {
	no pid
}

pred spawn[s: Service, p: Pid] {
	no s.pid
	p not in Service.pid
	pid' = pid + s->p
}

pred stutter {
	pid' = pid
}

fact traces {
	init
	always some s: Service, p: Pid | spawn[s, p] or stutter
}

pred sharing {
	some disj s, t : Service | s.pid = t.pid and some s.pid
}

run {}

check { 
	always not sharing
}

```

---

<div class="post-metadata">

**Author:** ![roehst](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/roehst/32/156_2.png) [@roehst](https://alloytools.discourse.group/u/roehst)\
**Post date:** [October 9, 2022, 5:42pm UTC](https://alloytools.discourse.group/t/hello-learning-alloy-can-someone-help-me-with-a-basic-question-on-temporal-models/288/3 "2022-10-09T17:42:06Z")

</div>

Hey, the `	pid' = pid + s->p` is super cool!

And the traces fact is also very useful.

Plus, changing the quantification strategy worked just fine!

Thanks a lot!