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

Questions
1

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:

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
image1870×430 19.7 KB

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

Thanks in advance

2

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.