Skip to content

CPS Assignment 1 Guide

Note

I have completed and explained only the first question (15M). The second question requires diagrams. Please check the end of Chapter-5.pdf for samples.

Subject & Subject Code

Cyber Physical Systems (Merged - CSIZG528/SEZG528/SSZG528)(S2-22)

Question Summary

Train Gate design in UPPAAL with prioritization of a train

Video Guide

Note

EDIT on 18-Apr-2023: There was a slight change in the code which I identified after recording the video. I have updated the code below accordingly. Please use the code below instead of the one that I showed in the video. The reorganize_queue() method below was changed to handle an edge case.

Check this video for a guide on how to solve the first question in the assignment: https://youtu.be/Anv6IKXWwis

Feel free to comment in the video if you have any doubts. Or contact me in the WhatsApp group. I will try to explain as much as I know.

Code

Global Declarations
/*
 * For more details about this example, see 
 * "Automatic Verification of Real-Time Communicating Systems by Constraint Solving", 
 * by Wang Yi, Paul Pettersson and Mats Daniels. In Proceedings of the 7th International
 * Conference on Formal Description Techniques, pages 223-238, North-Holland. 1994.
 */

const int N = 4;         // # trains
const int PRIORITY = 2;
typedef int[0,N-1] id_t;

chan        appr[N], stop[N], leave[N];
urgent chan go[N];
Train Declarations
clock x;
Gate Declarations
id_t list[N+1];
int[0,N] len;

void enqueue(id_t element)
{
        list[len++] = element;
}

void reorganize_queue() {
    int i;

    int elementIndex = -1;
    for (i = 0; i < len; i++) {
        if (list[i] == PRIORITY) {
            elementIndex = i;
        }
    }

    if (elementIndex != -1) {
        for (i = elementIndex; i > 0; i--) {
            list[i] = list[i - 1];
        }
        list[0] = PRIORITY;
    }
}

void dequeue()
{
        int i = 0;
        len -= 1;
        while (i < len)
        {
                list[i] = list[i + 1];
                i++;
        }
        list[i] = 0;
        reorganize_queue();
}

id_t front()
{
   return list[0];
}

id_t tail()
{
   return list[len - 1];
}
System Declarations
system Train, Gate;

Items to Submit for Q1

For Question 1, the following items need to be submitted:

  1. Uppaal XML file (explained in the video above)
  2. Description of working as PDF
  3. Properties used to verify

Don't ask me about Q2. Please figure it out. Because I myself have no idea about it yet.