02158 Concurrent Programming        Fall 2024
Spin: Tips and Tricks

Home

Plan

Material

General

• For Spin/JSpin installation see CP Lab 2 and the course wiki.
• JSpin cannot tolerate spaces in file paths - neither for the spin or dot programs nor the Promela files.

• If the automata generation is empty or does not reflect the current model, you may try to do a syntax check/verification on the model first.
• Note in if :: b -> S fi there is no implicit else-nothing branch - it just blocks until b becomes true. The else branch must be explicitly modelled: if :: b -> S :: else -> skip fi.

• When you verify LTL properties in SPIN observe that if you have more than a single instance of a process, you must specify the particular instance in the so-called remote reference. In particular, in P[i]@entry, the number i must be the instantiation number of the process (the one used in output from SPIN) and not the index within the family of P-processes as one might expect. Instance numbers belong to the predefined type pid.

   
  Instance numbers may be calculated from the number of active processes created. Alternatively, processes may be started explicitly by an init process and their instantiation numbers recorded in global values:

    pid up1, up2, down1, down2;
  
    init {
      atomic {
        up1 = run Car(UP);
        up2 = run Car(UP);
        down1 = run Car(DOWN);
        down2 = run Car(DOWN)
      }
    }
  
  

  Now you may refer to e.g. Car[up1]@entry in LTL-definitions. [For a more flexible solution you may, of course, use arrays of pid's]
• If an init process is used, it should appear as the first process.
• If you instantiate processes using run P(), be sure that proctype P() is not declared active too.
• If you check a global invariant I using a check process, the check should be applied repeatedly either by do :: assert(I) od or (!I -> assert(I)) (the latter being slightly more efficient). This will ensure that the check process only contributes with a single control point within the global state space.

• Use as small variable sizes as possible in order to reduce the size of the state vector (ie. the representation of a global state).
• Notice that the byte type is unsigned and wraps over.

• If you are using a version of Spin prior to 6.3.0 (see Spin output), you must adhere to the strict rules for using semicolon as described in [Spin].

Related to Mandatory Assignment 2

• In general, you may not be able to verify for all cars. If so, try to verify for fewer cars and discuss the coverage of your verification.
• Take care to ensure that your model faithfully reflects both the structure and the degree of atomicity of your Java solution.

Hans Henrik Løvengreen, Oct 3, 2024