# Learning temporal Alloy - Getting Alloy to do only one thing per time step

**URL:** <https://alloytools.discourse.group/t/learning-temporal-alloy-getting-alloy-to-do-only-one-thing-per-time-step/291>\
**Category:** Questions\
**Created:** [October 10, 2022, 8:39pm UTC](https://alloytools.discourse.group/t/learning-temporal-alloy-getting-alloy-to-do-only-one-thing-per-time-step/291 "2022-10-10T20:39:09Z")\
**Posts on this page:** 2\
**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:** [October 10, 2022, 8:39pm UTC](https://alloytools.discourse.group/t/learning-temporal-alloy-getting-alloy-to-do-only-one-thing-per-time-step/291/1 "2022-10-10T20:39:09Z")

</div>

Hi, I am modeling a simple system where people own stuff. There are a few ways to create and transfer stuff, but first I want to get alloy to show me one single change at a time.

The model is:

```auto
sig Thing {
}

sig Owner {
	var possessions : set Thing
}

pred createThing[t : Thing, o : Owner] {

	// Guard: no one owns this security
	o -> t not in possessions

	// Effect: stakeholder `a` owns this security
	possessions' = possessions + o -> t
}

pred init {
	no possessions
}

pred stutter {
	possessions' = possessions
}

pred owned[t : Thing] {
	t in Owner.possessions
}

fact traces {
	init;
	always {
		stutter or
		(one t : Thing, o : Owner | createThing[t, o])
	} 
}

run {
	eventually { all t : Thing | owned[t] }
} for 3 but exactly 3 Thing

```

This gives me the following example:

 ![image](https://global.discourse-cdn.com/free1/uploads/alloytools/original/1X/4b489cec4df2e3714e7ac60b2e92ba02c8a6a6fb.png)

How should I go about to get Alloy to only create only one new possession each time step?

Thanks in advance

---

<div class="post-metadata">

**Author:** ![alcino](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/alcino/32/25_2.png) [@alcino](https://alloytools.discourse.group/u/alcino)\
**Post date:** [October 11, 2022, 6:02pm UTC](https://alloytools.discourse.group/t/learning-temporal-alloy-getting-alloy-to-do-only-one-thing-per-time-step/291/2 "2022-10-11T18:02:06Z")

</div>

The main issue with your model is the `;` after the invocation of predicate `init`. Formula `a; b` means `a and after b`. This means that your fact `traces` is only enforcing stuttering or creates starting at the second transition. The first transition is unconstrained. If you remove the `;` it should work as expected. In general, I also recommend using quantifier `some` instead of `one` as the latter can sometimes have unexpected consequences.