Not strictly lecture notes, these are my own notes I have written based on what I have observed. They may not be factually correct, but are probably a damn bit easier to understand than other content

All code is taken from various bits of FSS, most of it the answer to Question 1 of the 2008-09 paper where applicable. There’s more comments about what the code is modelling there

1. You probably need a signature for things in the system, e.g. a Person.

   Sig Person{}

2. You need a State signature. This is the different bits and pieces and sets that make up the system at any one time. Any shorthand is reserved for functions, an example of which is below.

   fun State.council : set Person{this.(chair+ordinary)}
   
   sig State{
   	member : set Person,
   	served : set member,
   	chair : lone served,
   	ordinary : set member,
   	standing_as_chair : set member
   }

3. All states probably have to satisfy some constraints too, so put these in after the State signature like this.

   {
   	#ordinary =< 2
   	no chair & ordinary
   	standing_as_chair in served+council
   }

4. Now define your system operations, these are predicates. Some of them might just be a predicate that would be used to get data out, for example ‘count_number_of_times_rabbit_caught’. I expect in an exam, we’re probably not going to need to define anything like that, as it’s more focused on modelling the system correctly than modelling any utility predicates/functions.

   Predicates take in two states, any other input, and give out output. All of this is done through the parameters, including the output.

   Usually a predicate is of the form:

   1. Check everything is ok (preconditions)
   2. Make changes to the state
   3. Say that nothing else changes

   Here’s an example of quite a simple predicate:

   pred new_member[s,s' : State, p_in : Person]{
   	p_in not in s.member
   	s'.member = s.member+p_in
   	s'.chair = s.chair
   	s'.ordinary = s.ordinary
   	s'.standing_as_char = s.standing_as_chair
   }

   Note that the above predicate doesn’t have any output (apart from the new state). That’s fine. One that has an output might look like this:

   pred is_married[p_in : Person, q_out : lone Person, r, r' : Registrar]{
   	p_in in r.alive
   	q_out = r.partner[p_in] & (p_in in Man implies Woman else Man)
   	r' = r // no change
   }

   See what I mean about how they’re utility predicates?

   Some predicates can be nondeterministic. Here’s one:

   pred election[s,s' : State]{
   	s'.member = s.member
   	s'.chair in s.standing_as_chair
   	s'.served = s.served+s.council
   	no s'.standing_as_chair
   }

   Nothing wrong with nondeterminism as far as I can tell, just thought it was good to point out.

5. Unless told otherwise you probably need to model the initialisation too, something like:

   pred init[s' : State]{
   	s'.someset = none
   	s'.some_relation = none->none
   	s'.some_int = 0
   }

6. You may also need to give some Alloy commands. You may be told it’s unnecessary in an exam, but in Alloy itself you’d obviously need to otherwise the model can’t be used! If you’re unsure, try something like:

   go : run {} for 5 but exactly 1 State

   You can have checks too, which can be run to make sure your model does what you might expect. Practically, these are only really methods of debugging:

   death_undoes_birth: check {
   	all r, r_m, r' : Registrar, p : Person |
   		birth[p, r, r_m] and death[p, r_m, r'] implies r.alive = r'.alive
   } for 5 but exactly 3 Registrar

7. Done! Enjoy your State-based Model!