So far, we've seen some of the built-in checks performed by SPIN: assertions, deadlock, non-progress, and one notion of fairness. But what about other properties we'd like to check for? We might be interested in properties which the implementors of our particular tool weren't interested in, or hadn't thought of. Fortunately, SPIN does include a general property-checking mechanism: If we can state our property in a particular formal temporal logic, then SPIN will allow us to check the property. First, we'll introduce the syntax and semantics of one particular temporal logic, LTL. Then, we'll return we'll return to SPIN and how it uses temporal logic for verification. First, we reflect that some properties — safety properties — can be phrased in terms of ``some particular state is unreachable''. For example, a state where two processes are sending information to the printer simultaneously never occurs. Failed assertions can be viewed as a transition to a fail-state, and we require that this state is unreachable. Deadlock can be viewed as a state with no legal outgoing transition, and not all processes sitting in an end-state. Similarly we reflect that other properties — liveness properties — are about entire traces, not just some state in a trace. For instance, non-progress cycles is a cycle which does not contain any states labeled as progress states. We want a richer language to have a way of talking about traces, but that is precise and not subject to English's vagaries. We'll work towards using logic — a temporal logic specifically designed to be conducive to expressing concepts which arise in concurrent programming. But before we can even do that, we need a clear model of concurrent programs, and more formal definitions of some ideas we've already seen.

Concurrent Programs as State Space Automata The notions we've seen of states, traces, and state spaces aren't specific to Promela, but are useful in any formalization of concurrent systems. In fact, we are ready to give one precise definition of a ``concurrent system'' in terms states and traces. It is similar to many conventional automata definitions, but includes a way to relate the current state to propositions, which we can later construct formulas out of. State Space Automaton A State Space Automaton A is a tuple S s0 T Prop P where: S is a set of states. As before, a state is an assignment to all program variables (both local an global), including the program counter (line number) for each process. s0 S is the initial state or start state. T S S is the transition relation. Equivalently, this is the edge relation of the state space. Prop, a set of propositions. P : S→2Prop is a mapping which, given a state, indicates all the properties that are true in that state. It is the set Prop which will allow us to talk about our program variables in our logic formulas. The elements of Prop are simple propositions involving program variables. For example, philosopher_2_has_fork (ctr3) (in[].size() == max_buffer_size) (that is, the buffer in[] is full) Each of these might be true in some states and false in other states; the function P gives a truth assignment to the propositions (a different truth assignment for each state). Trace Given a state space automaton, a trace σ (sometimes called an ω-trace) is a (possibly infinite) sequence of states σ0, σ1, σ2, … which respects the automaton's transtion relation T. Thus a trace is a path through the state space (as we have already seen). Now that we have logic propositions associated with each state, we can see that during a trace, those propositions will change their truth value over time. We'll illustrate this with diagrams like the following.

A timing diagram for a trace σ, and propositions p and q. Each propositional variable's value during the trace is depicted as a line. When the line is high, the proposition is true; when low, false. In this example, p and q are propositions from Prop. Since in the trace σ, we have p being true at (for example) index 2, we write σ2 ⊧ p. In this diagram, it is also the case that σ0 ⊧ (p∨q). Technically, these diagrams are a bit too suggestive: a trace is only a sequence of discrete states, with no concept of time existing in between states. And the numbering of the x-axis is only an index to the sequence of states — it's not meant to imply that the system's states necessarily correspond to periodic samplings of our program. Yes, it would be more accurate to replace these continuous timelines with a textual list of and (to represent the automaton's mapping P). However, the diagrams better communicate information to us humans, especially those familiar with such timelines as used by hardware circuit designers. We just need to be careful not to read in between the times. Although a bit unintuitive at first, it will be convenient to convert all finite traces into infinite ones. To do the conversion, we simply envision that once the automaton reaches its ostensibly last (nth) state, it languishes furiously in that state over and over: Stutter-Extend The finite trace σ0,…,σn can be stutter-extended to the infinite trace σ0, …, σn, σn, σn, … . To ensure this still satisfies the definition of a trace (where successive states must obey the automaton's transition relation), it is often assumed that every state has a transition to itself. Note that this convention precludes assuming that something must change between one state and the next, which is plausible since we are modeling asynchronous systems. This will be reflected in our formal logic below, which will have no built-in primitive for ``the-next-state''.

State Formulas Now that we have a formal model of what a trace is, we can start to make formal statements about what happens in a trace. The simplest statements are state formulas, i.e., propositional formulas built out of Prop. For a given trace σ and state formula ψ, we can immediately decide whether a particular state σi satisifes ψ (notationally, ``σi ⊧ ψ''). Deciding whether some particular state of a trace satisfies a formula also depends implicitly on the automaton Σ. Technically we should write Σ,σi ⊧ ψ, though in practice Σ is clear from context. For example, given a trace σ, we might ask about what is happening at σ957, and whether σ957 ⊧ ¬Proc1_is_printing, or whether σ957 ⊧ ((ctr3)→philosopher_2_has_fork). The answer would be found by taking the automaton's function P, and seeing what values the truth assignment P σ957 assigns to our formula's individual propositions such as (ctr3). Consider the trace σ we saw previously and is repeated here.

A timing diagram for a trace σ, and propositions p and q. For which i does σi ⊧ (p∧q)? For which i does σi ⊧ (p∨q)? How about σi ⊧ (p→q)? However it doesn't make sense a priori to ask whether an entire trace satisfies some particular state formula; unlike regular propositional logic, the truth of state formulas changes over time, as the trace σ progresses.

Introducing Temporal Connectives So, how do we talk about formulas holding (or not) over time? In addition to making formulas out of ∧,∨,¬ and propositions from the set Prop, we'll allow the use of temporal connectives. □ — always, or henceforth: We say that □φ is true at a moment i, iff φ is true from moment i onwards. ◇ — eventually: We say that ◇φ is true at moment i, iff φ will eventually be true at moment i or later. U — strong until: We say that (φUψ) is true at moment i, iff ψ eventually becomes true, and until then φ is true. W — weak until: Like Strong Until, but without the requirement that ψ eventually becomes true. As a mnemonic for the symbols ``□'' and ``◇'', we can imagine a square block of wood sitting on a table. Orienting it like □, it will always sit there; orienting it like ◇, it will eventually teeter. More formally, we define these connectives as follows. Always σi ⊧ □φ iff ∀j≥i. σj ⊧ φ

A generic trace σ satisfying σi ⊧ □p. p is true in state i and all later states. Decide whether each is true or false for following trace σ (the same one seen earlier).

A timing diagram for a trace σ, and propositions p and q σ9 ⊧ □q σ9 ⊧ □¬p σ0 ⊧ □q σ0 ⊧ □(p→q) True; from σ9 onwards, q stays true. True. Even stronger, σ7 ⊧ □¬p. False, since σ3 ⊭ q. True, since at each individual index i (from 0 on up), σi ⊧ (p→q). Eventually σi ⊧ ◇φ iff ∃k≥i. σk ⊧ φ

A generic trace σ satisfying σi ⊧ ◇q. q is true in some state k after state i. Decide whether each is true or false for the trace σ seen earlier. σ9 ⊧ ◇p σ9 ⊧ ◇¬p σ0 ⊧ ◇q σ0 ⊧ ◇¬q σ9 ⊧ ◇(q→p) σ0 ⊧ ◇¬(p→q) False; from σ9 onwards, p stays false. True. This is a much weaker statement than σ9 ⊧ □¬p, which we already saw was true. Extremely true, since q is already true in σ0 (and elsewhere, too). True, since ¬q is true in σ3 (and elsewhere too). False. False. We already mentioned that σ0 ⊧ □(p→q); if you think about it, this means that σ0 ⊧ ¬ ◇¬(p→q) . (While we won't spend time discussing algebraic equivalences for LTL formulas, this is certainly reminiscent of DeMorgan's Law.) Before continuing on with our two other connectives (strong- and weak-until), let's pull back a bit and look at our notation. The nit-picky — er, the careful reader will have noticed that although we write σi ⊧ …, really, the truth value of the formula depends not on just a single state, but rather that state and the entire suffix of the trace after that. So writing σ i ⊧ … would be more accurate. Moreover, we are using not just the trace but also the timing diagrams, which are just the graph of an automaton A's mapping function (``P''). Thus the correct formulation really needs to be written A σ i ⊧ … (and it is required that σ be a legal trace with respect to the transitions of A). However, now that we realize our abuse of notation, we'll revert and just write σi ⊧ …. In practice, we are often considering an entire trace, and wondering whether some property holds always or eventually. It's extremely natural to extend our notation from particular indices to the trace itself: Trace σ models formula φ (``σ ⊧ φ'') iff σ0 ⊧ φ. For example, from the above exercises, since σ0 ⊧ (p→q), we say simply σ ⊧ (p→q). Strong Until σi ⊧ (φUψ) iff ∃ki. (σk ⊧ ψ∧∀j. ( i ≤ j < k →σj ⊧ φ) ) .

A generic trace σ satisfying σi ⊧ (rUs). r is true in states i through (k1). Decide whether each is true or false for following trace σ: (This is the same trace seen earlier.)

A timing diagram for a trace σ, and propositions p and q. σ0 ⊧ (qUp) σ2 ⊧ (qUp) σ5 ⊧ (qUp) σ9 ⊧ (qUp) True. q is true in σ0, and it doesn't take long before p becomes true in σ1. False. Starting at σ2, we see that p doesn't become true until σ5, yet q doesn't stay true that long. Very true, since p is already true in σ5. (In the definition, take k=5; then there are not any j to even need to worry about.) False. Since p is from σ9 onward, we can't even find a (k9) such that σk ⊧ p. However, it is true that σ9 ⊧ (qWp). Give the formal semantics of Weak Until (in the same way we have given semantics for □, ◇, and Strong Until). σi ⊧ (φWψ) iff (∀j≥i. σj ⊧ φ ∨(∃ k ≥ i . σk ⊧ ψ ∧∀ i ≤ j < k . σj ⊧ φ )) Weak Until could be omitted from our core set of LTL connectives, since it can be defined in terms of the remaining connectives. Provide such a definition. That is, give an LTL formula equivalent to (φWψ). Here are three equivalent definitions. The first follows directly from the above exercise. (φWψ)≡(□φ∨(φUψ)) (φWψ)≡(◇¬φ→(φUψ)) (φWψ)≡(φU(ψ∨□φ)) Any logic that includes temporal connectives is a temporal logic. More specifically, this is Linear Temporal Logic (LTL). The ``linear'' part of this name means that we are looking only at individual traces, rather than making formulas that discuss all possible traces of a program. After all, a single program can result in many possible traces. An LTL formula does not allow us to say, for example, that a property holds in all possible executions of the program. However, SPIN overcomes some limitations by essentially testing an LTL formula against all possible traces. Will will return to SPIN in the next section. In summary, the syntax used in SPIN is given by the following grammar. SPIN's Grammar for LTL formulas ltl ::= atom | (ltl binop ltl) | unop ltl | (ltl) unop ::= [] ``Always'' | <> ``Eventually'' | ! ``Not''binop ::= U ``Strong Until'' | W ``Weak Until'' | && ``And'' | || ``Or''atom ::= true | false | name #define'd identifiers

Some presentations of LTL use a box or ``G'' (Globally) for Always, and use a diamond or ``F'' for Eventually. Confusingly, some use ``U'' for Weak Until. Also, some include additional connectives like ``X'' (Next), which cannot be defined in terms of those given.

Do we really need a whole new logic? We could use regular ol' first-order logic as our formal language for specifying temporal properties. We'd do this by adding an explicit time index to each proposition in Prop, turning it into a unary relation. For example, instead of considering Philosopher_B_has_fork in state 17, we'd instead write Philosopher_B_has_fork⁡(17), and so on. This approach, though, quickly becomes cumbersome. Consider the everyday concept ``Someday, X will happen''. We have to go through some contortions to shoehorn this concept into first-order logic: ``There exists a day d, such that d is today or later, and X will happen on d''. Quite a mouthful for what is about the simplest temporal concept possible! The awkwardness stems from the fact that in English, ``eventually'', ``always'', and ``until'' are primitives. When we design a formal language to capture with these concepts, shouldn't we too include them as primitives? Having our formal representations reflect our natural conceptions of problems is the first law of programming! This is why we have decided to incur the overhead of defining a new language, LTL. Still, you have noticed that the semantics we've given are phrased in terms of ``∀i.…''. From a language designer's perspective, we might say that LTL is a high-level language, and we give an interpreter for it written in first-order logic (over the domain of trace-indices).

Translating between English and LTL: Examples Let's look at how to turn a natural-English specification into temporal logic, and vice versa. How might we express the common client/server relationship ``if there is a request (r), then it will be serviced (s)''? Hmm, that seems obvious: (r→s) should do it, no? Alas, no. The problem is, the truth of this formula — which has no temporal connectives at all — only depends upon the trace's initial state, σ0 — in this case, whether σ0 ⊧ (¬r∨s). This certainly doesn't match our intent, since we want the request and service to be able to happen at points in the future. Let's try again… Does the formula □(r→s) capture the English notion ``if r is true, then s will be true''? That's only a bit better: it does now allow the implication (r→s) to hold in any state σi. But our intent is to allow the servicing s to happen after the request r. The formula as given only expresses ``Whenever r is true, then s is also true at that moment.'' If r and ¬s both hold at the same time (which wouldn't be surprising), then □(r→s) fails for that trace. After more thought, we can get something which does arguably match our intent: □(r→◇s). ``Whenever a request is made, a servicing will eventually happen.'' However, even this may not be what everybody wants. Some considerations: Even if r is raised (and lowered) several times, a single moment of s can satisfy the entire trace. This matches an intuition of r indicating a single ring of a telephone (and s being `pick up the phone'), but may not match the intuition of r being ``leave a voicemail'' (and s being ``respond to a voicemail'').

A trace showing multiple requests followed by a single servicing. A trace in which s is always true (regardless of r) certainly satisfies φ. Did you expect the English statement to encompass this? Any trace in which requests are serviced instantaneously will satisfy φ. While this might be intended, it might also be a bug of leftover servicings from previous requests.

A trace showing multiple requests and a single servicing. The servicing arguably corresponds to only the first request and might be an undesired behavior. A trace in which a request is never made still satisfies this formula. While that is probably what is intended, it may not have occurred to you from the English statement alone. One advantage to having a formal language is that because the semantics are precisely defined, it helps us think about corner cases such as the above (and, gives an unambiguous meaning to the result, good for writing specs). As a more complicated variation, we generally want to match requests and their servicing. For example, what if there are two requests, r1 and r2, arriving in that order? In a particular context, do we expect that there are also exactly two servicings, s1 and s2? If so, do we also expect them in that order? As a partial solution, how can we express ``whenever r1, s1 will happen before s2''? If we are also requiring that s2 indeed actually happen, then we can use the following: □ ((r1∧◇s2)→(¬s2Us1)) . Note that since LTL does not have quantifiers (like ∀ and ∃) we cannot use variable indexing in our formulas. In other words, we can't talk about ri and sj, but instead, must always refer to specific variables like r1 and s2. From these examples and the ones following, we can see that English is typically too ambiguous. To get the appropriate logic formula, we need to go back to the original problem and determine what was truly meant. Formalizing your specifications into temporal logic gives you the opportunity to closely examine what those specifications really should be. Given a formula, try to understand it by translating it into English. Providing sample timelines that satisfy the formula is also quite helpful. Describe the meaning of □◇p in words and a timeline. Literally, we can simply say ``always, eventually p''. While that phrase is fairly common among logicians, it's not very natural or meaningful to most people. A clearer, but more long-winded, equivalent is ``at any point in time, p will happen in the future''. More concise, though, is ``p happens infinitely often''. To understand that, consider a timeline. In words, at any time t0, p will happen sometime in the future; call that time t1. And at moment t1+1, p will happen sometime in the future; call that t2. Repeat forever.

The beginning of a trace where p happens infinitely often. Describe the meaning of □(q→□¬p) in words and a timeline. Again, a literal translation is ``always, if q then always not p''. Correct, but a bit more idiomatic-English would be ``whenever q, then forever not p'' or ``Once q, p is forever false''.

The beginning of a trace satisfying the property. A railroad wants to make a new controller for single-track railroad crossings. Naturally, they don't want any accidents with cars at the crossing, so they want to verify their controller. Their propositions Prop include train_is_approaching, train_is_crossing, light_is_flashing, and gate_is_down. Brainstorming: Using natural English, what are some properties we'd like to have true? Feel free to use words like ``always'', ``eventually'', ``while'', and ``until''. You may add new propositions to Prop, if you think it's appropriate. For each, feel free to demonstrate that the one property is not sufficient: give a trace which satisfies the property but is either unacceptable or unrealistic. (For instance, ``the gate is always down'' is safe but unacceptable; ``a train is always crossing'' is unrealistic since there aren't infinite trains.) We can think of lots of examples, such as these. Whenever a train passing, the gate is down. If a train is approaching or passing, then the light is flashing. If the gate is up and the light is not flashing, then no train is passing or approaching. If a train is approaching, the gate will be down before the train passes. If a train has finished passing, then later the gate will be up. The gate will be up infinitely many times. If a train is approaching, then it will be passing, and later it will be done passing with no train approaching. (Thus, trains aren't infinitely long, and there are gaps between the trains.) To formalize such statements, we would start with the primitive propositions involved. These could be a (``a train is approaching the crossing'') p (``a train is passing the crossing'') l (``the light is flashing'') g (``the gate is down'') This choice forces us to not refer to individual trains and, thus we must simplify some of our properties, e.g., ``If a train is approaching, the gate will be down before the next train passes.'' (Think about the consequences of not making this change.) Some of these English descriptions are ambiguous, however. E.g., can a single train be approaching and passing simultaneously? When writing formal specifications, we'll be forced to think about what we mean to say, and provide an unambiguous answer, one way or the other. Continuing this example, we'll say that once a train is passing, it is no longer considered to be approaching. Encode some of the properties from the previous exercise in temporal logic. It is often helpful to first turn the statement into a timeline (essentially a trace). ``Whenever a train passing, the gate is down.'' ``If a train is approaching or passing, then the light is flashing.'' ``If the gate is up and the light is not flashing, then no train is passing or approaching.'' ``If a train is approaching, the gate will be down before the next train passes.'' ``If a train has finished passing, then later the gate will be up.'' ``The gate will be up infinitely many times.'' ``If a train is approaching, then it will be passing, and later it will be done passing with no train approaching.'' Keep in mind that for any concept, there are many different (but equivalent) formulas for expressing it. □(p→g) □((a∨p)→l) □ ((¬g∧¬l)→(¬p∨¬a))

A trace satisfying this property. Observe in the trace shown that in one instance, the gate goes down at the same time the train passes. In the LTL version we're using, we can't express the idea ``… strictly before the next train passes.'' Instead, we'll allow this simultaneity as a possibility. □ (a→(¬pWg)) I.e., if a train is approaching, then a train is not passing until the gate is down. However, this still allows that the gate could be back up by the time a train passes, and a train might never pass.

A trace satisfying this property. □ ((pU¬p)→◇ (¬p→◇g) ) Since our logic cannot talk about the past, we have to shift our perspective to start while the train is still passing. We've effectively reworded the statement to say that if a train is passing and will finish passing, then sometime after it is no longer passing, the gate will be up. However, the status of the gate at other times is not commented on. We're only saying there is one moment after the train passes that the gate is up. □◇¬g

A trace satisfying this property. □ (a→◇ (p∧◇ (¬p∧¬a) ) ) This last condition is not something that a controller would enforce. Instead, we would expect the train scheduling software to enforce this. The controller would be allowed to assume this, and we'd want to verify a property ψ only for traces that also satisfy our scheduling assumptions φ. Of course, we can also do this by incorporating assumptions into the formulas: (φ→ψ). We've previously seen that SPIN knows some built-in concepts such as deadlock, livelock, weak- and strong-fairness. We'll see in the next section that SPIN can also be used to verify any LTL formula. But first, let's characterize some of those built-in concepts as LTL formulas using the context of a print server. We will use the following propositions: b : This is a bad state. (It corresponds to Promela assert(!b)). e : This is a valid end state. (It corresponds to all Promela processes being at an end label). p1, p2: Progress is being made (either of two types of progress); they correspond to a Promela process being at a certain progress label.Promela does includes a handy syntax for testing whether a particular process is at a particular label: ``philosopher[3]@eating'' is true when the fourth (0-indexed) philosopher process is at the label eating. r: There is a pending request. s: A request is being serviced. Give a temporal formula expressing each of the following: No error occurs, i.e., we never reach a bad state. No deadlock occurs. (We'll take deadlock here to mean that all five of our variables stop changing; without having a different proposition for each state, this is close enough.) Progress is always made. That is, this trace doesn't go forever without making progress. Weak Fairness: if a request is made and held, it will get serviced. I.e., it's not the case that a request stays forever but is never serviced. Strong Fairness: if a request is made infinitely often, then it will be serviced. For each of these problems, there are many equivalent formulas, some of which are easier to verify as equivalent than others. □ ¬ b ¬ ◇ ((□b∨□¬b)∧(□p∨□¬p)∧(□r∨□¬r)∧(□s∨□¬s)∧□¬e) . Remember that if we're in an end-state, then it doesn't count as deadlock. □ ◇ (p1∨p2) ≡(□◇p1∨□◇p2). In fact, SPIN provides a built-in variable np_, which corresponds to ``all processes are in a non-progress state''. When SPIN does its built-in check for non-progress cycles, it actually just verifying !<>[]np_. You might recall that SPIN's idea of progress is state-based, not transition-based: SPIN (counterintuitively) considers it progress when a process does nothing but squat in a progress state. (This can only happen if weak fairness is not being enforced, or a guard is being labeled as progress.) How might we capture ``progress'' but still preclude those traces which just sit idly at a progress label? We could add a second progress label immediately following p1, call it q1. Similarly, we can introduce q2. Then we could verify that ((□◇p1∧□◇q1)∨(□◇p1∧□◇q1)). (This assumes that all labels are private to each process.) ``It's always not the case that r is always on, and yet s doesn't happen an infinite number of times'': ¬ □ (□r∧¬□◇s) . One equivalent formula is ``if r stays on forever, then it's being serviced infinitely often.'': □ (□r→□◇s) . (□◇r→□◇s) For our simple producer/consumer model, what is the basic property we'd like to guarantee? Roughly, ``each product is consumed exactly once''. That is, Produce and Consume are called alternatingly, starting with Produce. (In particular, as stated this precludes modeling ``produce twice and queue the results''.) Expressing this actually requires several clauses. Give colloquial English translations of the following LTL formulas. We can make the generic model a bit concrete by interpreting startProduce and finishProduce as starting and finishing the production of a fine, hand-crafted ale, with startConsume, finishConsume corresponding to enjoying such an ale. (The more health-concious reader might prefer to instead interpret these as start/finish the training for a marathon, and start/finish running a marathon, respectively.) □ (finishProduce→◇startConsume) □ (finishProduce→(¬startProduceUfinishConsume)) (¬startConsumeWfinishProduce) □ (finishConsume→(¬startConsumeWfinishProduce)) If an ale is produced, then an ale will be consumed (possibly immediately). Note that we don't talk about which ale is consumed; in the following clauses we will try to enforce that it really is the same ale that was recently produced. If an ale is produced, then no ale-production is started until after an ale has been consumed. No ale is consumed before (an initial) ale is produced. Note that a trace in which no ale is ever produced still satisfies this formula. If an ale is consumed, nothing else will be consumed until an(other) ale has been produced. In the previous exercise, the formulas entailed that production of an item could not even begin until the previous object had been entirely consumed. This requirement might make sense for the interpretation of marathon training/running, but it doesn't seem essential to the production of hand-crafted ale, even if we do want to preserve the policy of never queuing up products. Suppose we have a computer network port whose buffer can store only one web page's data at a time. The producer could correspond to some server sending a web page to that computer, and the consumer might be a browser which processes the data being received. Do we want to allow the producer to be producing the next product before the consumer finishes the current one? What change would you make to the formulas if you did want to allow this produce-while-consuming behavior (as in the ale interpretation)? No. That would mean the buffer is being overwritten with a new web-page's data, even though the browser is still trying to process the current page in the buffer. We would replace □ (finishProduce→(¬startProduceUfinishConsume)) with □ (finishProduce→(¬finishProduceUfinishConsume)) . Note that we want to include the possibility that nothing is ever produced — we don't always want to enforce weak fairness. Consider an operating system's code for a print server — it is truly important that not owning a printer doesn't mean the OS always crashes! Through this section, we've seen some of the common patterns that can arise in the formulas. Following upon the idea of Design Patterns as describing common programming idioms, ``Specification Patterns'' describe common logic specification idioms. For a list of LTL specification patterns, see Property Pattern Mappings for LTL. In addition, there are also algebraic equivalences for LTL, just as there are for propositional logic. We have already seen a DeMorgan-like example; there are also less obvious equivalences, such as distributing □◇ over ∨: □◇(φ∨ψ)≡(□◇φ∨□◇ψ) and the redundancy of □-over-∨: (□φ∨□ψ)≡□ (□φ∨□ψ) It can be fun to dabble in rewriting LTL formulas, but (alas) we won't visit that topic further here.

Using Temporal Logic in SPIN So, we have a Promela program and an LTL formula to verify. How do we use the tool? In SPIN, in the "Run" menu, select "LTL Property Manager". This opens a new window. The top half contains several subparts for entering an LTL formula, while the bottom half is for using it. In the "Formula" textbox, you can type an LTL formula. If you prefer, you can enter the operators using the buttons below, rather than typing. Also, you can use the "Load" button to restore a previously-saved LTL formula from a file. For a formula, the next checkboxes allow you to either verify that the formula always holds or never holds. The "Notes" textbox is simply descriptive text. If you plan on saving the formula, it is helpful to remind yourself what this formula means and is used for. The "Symbol Definitions" textbox is where the LTL variables (typically p, q, etc.) are related to the Promela code. This is done through #defines which are temporarily added to your Promela code. Let's consider another critical section example. The following code simply puts the critical section into a loop. Also included is our standard code to check that the mutual exclusion property is satisfied, although the assertion is commented out.


 1  /* Number of copies of the process to run. */
 2  #define NUM_PROCS 3
 3
 4  show bool locked = false;
 5  show int  num_crit = 0;
 6
 7  active[NUM_PROCS] proctype loop()
 8  {
 9    do
10    :: true ->
11
12       atomic {
13         !locked ->
14         locked = true;
15       }
16            
17       /* Critical section of code. */
18       /* Something interesting would go here. */
19            
20       num_crit++;
21       /* assert(num_crit == 1); */
22       num_crit--;
23            
24       locked = false;
25       /* End critical section of code. */
26    od;
27  }

Using temporal logic, we can accomplish the same check without the assertion. There are several similar ways of doing this. One way is to verify that num_crit always has the value 0 or 1. To do this, we'll make the following definition in xspin's ``Symbol Definitions'' textbox:


#define p ((num_crit == 0) || (num_crit == 1))

We then want to verify that p always holds, so our formula is []p and mark that we always want this formula to hold. To verify with this formula is a two-step process. First, using the "Generate" button generates what is known as a never claim, shown in the window. This is more Promela code that is temporarily added to your program. This creates a special process that checks the LTL formula and is guaranteed to be executed after every normal step of your code. You don't need to understand the generated never claim, although SPIN presents it for advanced users. The never claim uses a couple syntactic features of Promela not covered in this module. Next, using the "Run Verification" button opens a small version of the verification options window that we're already familiar with. Running the verification puts any output in the LTL window. To verify temporal formulas from the command-line, you need to do three things: First, generate a never claim using spin -f formula. For example,


prompt>  spin -f '[] (p ->  <> (q || !r))'

Be sure to quote the formula so the shell doesn't try to interpret special characters. Next, take the output (which is Promela code for a never claim), and paste it at the end of your Promela source file. Also add #defines to the top of your file, defining each propositional variable used in your LTL formula. Finally, verify the resulting code. Generate and verify the code from the previous example. The automatically-generated never claim is shown below. It uses labels and gotos which we haven't discussed, but which will be familiar to many programmers. (This code represents a small automaton, in this case with two states, which gets incorporated into the larger state space automaton that we've described.) The use of the constant 1 here is equivalent to the more mnemonic true.


never {    /* !([]p) */
T0_init:
        if
        :: (! ((p))) -> goto accept_all
        :: (1) -> goto T0_init
        fi;
accept_all
        skip
}

Running the verification, it does not report any errors. However, note that verifying an LTL property automatically turns off deadlock checking:


Full statespace search for:
        …
        invalid end states      - (disabled by never claim)

However, it still reports a warning that the process never exits, in case we care:


unreached in proctype loop
        line 27, "pan.___", state 11, "-end-"
        (1 of 11 states)

We want to accomplish the same goal as the previous example, but with a formula that should never hold. What's an appropriate formula? Using the same definition of p, we can simply use <>!p. I.e., we don't want it to ever happen that p is false. Now let's verify something that can't be done easily with just assertions. We also want to make sure that num_crit continually alternates between the values of 0 and 1, rather than maintaining the same value. How can we do this? Use the following symbol definitions:


#define p (num_crit == 0)
#define q (num_crit == 1)

and verify that


([]<>p) && ([]<>q)

always holds. How could we use LTL to verify whether no process is starved? Of course, this verification should fail, generating a trail where at least one process is in fact starved. In essence, we want to verify


([]<>(_pid == 0)) && ([]<>(_pid == 1)) && ([]<>(_pid == 2))

The problem is that _pid is a local variable to each process, but, unfortunately, never claims are their own separate process, and can't access those variables. One solution is to create an equivalent global variable:


pid running;

Inside the critical section code add the line


running = _pid;

Use the following symbol definitions:


#define p (running == 0)
#define q (running == 1)
#define r (running == 2)

and verify whether


([]<>p) && ([]<>q) && ([]<>r)

always holds. The never claim's process will numbered higher than any started by an active proctype. So, in this case, its PID is 3. As expected, the verification fails, and a trail file is created. In the author's sample verification, this trail has only processes 0 and 1 entering the critical section, although there are many possible counter-examples. It turns out, SPIN has a special syntax to express whether a certain process is at a certain label. So instead of defining a new variable, we could alternately go to the critical section and add a new label (say ``crit:'') and then define:


#define p (loop[0]@crit)   /* 0th 'loop' process is at crit. */
#define q (loop[1]@crit)   /* 1st 'loop' process is at crit. */
#define r (loop[2]@crit)   /* 2nd 'loop' process is at crit. */