State Based to Trace Based, an example

This might be wrong...

These are lecture notes from my Computer Science course, not a general reference for "State Based to Trace Based, an example"

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

This is running through the answer to Question 3v on the 2007-08 paper, and assumes you at least have an idea about what trace-based specifications are meant to be doing

1. Think about what each event in the trace-based model needs to store, for example an element of a queue.

2. You need a few simple lines to define events. These are roughly the same every time:

   open util/ordering[Event] as trace
   sig Element{} -- here's what I mentioned in step 1
   abstract sig Event{ value : Element }

3. Now you need to extend the Event signature. Take a look at your predicates in your state-based model.

   Sig Enqueue, Dequeue extends Event{}

4. It’s unlikely, but maybe you had a constant in your state-based model? In which case you’ll need one here too:

   one sig Max{length : Int}{0 < length}

5. From what I’ve seen, you can cleanly put simple state-based models into a single trace-based predicate. But you don’t need to (see other examples).

   pred q{
     all e : Event | let pfx=prevs[e],
                     size = #(pfx&Enqueue) - #(pfx&Dequeue)
     {
       e in Enqueue implies size < Max.length
       e in Dequeue implies {
         0 < size
         e.value={x : Enqueue | #(prevs[x]&Enqueue) = #(pfx&Dequeue)}.value
       }
     }
   }
   
   

   Line 2: you want to define that the predicate holds for all events. Then you want to define (with the let bit) any values you’re going to use. For example, here size is the number of Enqueue events minus the number of dequeue events, which intuitively gives the size of the queue.

   Lines 3-7: denote the preconditions for each event. Unfortunately there’s no ‘rules’ you can follow to construct these preconditions, you just need to learn to have the ‘knack’ for writing Alloy :(

Functions

In trace-based specifications you might need to use a function to return a set of data about the history behind each event. For example in the rabbit_trace.als example, you often need to know about the tags in use at any point in time. Here’s an example where you want to find a set of ‘Item’s in the history of an event that is available in certain events called ‘Item_Made’ but also don’t want to include any that have been ‘Item_Destroy’ed.

fun Event.items_available = set Item {
	let pfx = prevs[this] | 
		{ i : Item {
			some e : Item\_Made&pfx {
				i in e.item-(Item\_Destroy&pfx&nexts[e]).item
			}
		}
}

Note the importance of specifying that the events must be in the prefix, otherwise it could be any event anywhere.

Other notes

• No state, just events
• You can split the predicates up if it makes you feel better. See listing 1 on JJ’s paper (CS York login required)
• When thinking about predicates, think about all the preconditions the events need, for example you can only destroy items that have already been made, you can only switch off a radio that is on.

Comments