02152 Concurrent Systems        Fall 2008
Mandatory Assignment 1: Update Page

Home

Plan

Material

 
This is the update page for Mandatory Assignment 1: Car Control. Please consult that page for the problem description.

Some Pieces of SPIN Advice

For those of you that may have started late on the SPIN part, here are some common problems encountered.

• 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]@alleystart, 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 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 you get an error at a very large search depth, try to halve the search depth until you exceed the search depth. Then go back and use the built-in option to reduce to shortest error trail.
• 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.
• In Step 2, your priorities should be as follows:

  1. Get the model right so that it soundly reflects your program code.
  2. Verify the safety property. If this is not possible, try to identify the problem from a shortest error trail. If you can easily fix the problem do so. If not, comment on the problem and stop there.
  3. Try to verify the liveness properties. Use CP lab 3 as a starting point. As above, if you cannot verify, try to identify the problem. If not possible, stop. Remember that your solution need not be fair!

Amendments

Errata and clarifications to the assigment.

• Sep 24: A performance deficiency in the GUI has been fixed. Please reload mandat1.jar or just the file Cars.java.

FAQ

 

None yet

Practical Issues

• Each group must hand in one copy of the report on paper. The report must be signed by all group members (cf. general report requirements).

   
  Your group number should appear on the front page.

  See also the slides with advices on the reporting (ps)(pdf) and the general reporting requirments.

• The paper report should contain easily idenfiable printouts of the files CarControl.java and CarTest.java (as well as any auxiliary file you may have added) for each version of your system.

   
  Thus, all modified Java classes must be present in the report as appendices. Also your Promela and LTL-property files must be included.

• Additionally, the files must be handed in electronically for potential testing. For each version, both the source files as well as the compiled .class files must be collected in a .jar file. The source files must be identical to the printouts in the report.

  To create a .jar file for the version being the answer to Step no. n, in the directory where both the source files and the corresponding class files are present, issue the command:

  jar cMvf step_n.jar *.java *.class

   
  [Note that n is a syntactic variable that must be substituted by the step number, e.g. step_3.jar]

  You may consult the manual pages for the jar command in order to understand the precise effects of the command line.

  Alternatively, you may prepare the jar-file as an executable application using a Manifest file (eg. generated by a development environment like Eclipse).

  If properly done, it should be possible to run the program out-of-the-jar by issuing the command:

  java -classpath step_n.jar Cars

   
  Or, alternatively as an application using

  java -jar step_n.jar

   
  You must check that the .jar-files can run this way before submitting them. The programs will be tested in the JDK 1.6 environment.

  You are requested to deliver electronically the versions corresponding to Step 3 (including Step 1), and Step 5 (including Step 4), i.e. step_3.jar, and step_5.jar. You might also deliver separate versions for steps 1 and 4.

  If you have have done any EXTRAs, they should be identified in the version number, eg. step_4C.jar for a solution to Step 4 with fair alley synchronization.

  Otherwise, alternative version may be identified like step_3_alt.jar etc.

• For Step 2 the Promela and possibly LTL-files must be packed into an archive using either .zip, .tar, .tgz or .jar formats. The archive file should be named step_2.zip (similarly for other formats).

   
  The same applies if you have done EXTRA (A), ie. the file should be packed eg. as step_3A.zip.

• The archive files must be delivered as attachments to a single mail sent to c02152@imm.dtu.dk.

   
  The subject line of the mail must be "Man1-NN" where NN is your two-digit group number, e.g. Man1-47

  The format of the body of the mail is free, but must comprise your student numbers and names for identification purposes as well as an indication of the versions provided and the EXTRAs you may have done.

  The mail must be sent before the deadline.

Hans Henrik Løvengreen, Oct 10, 2008