//This file was generated from (Academic) UPPAAL 4.1.3 (rev. 4455), November 2009

/*

*/
inf {Task(0).EndPeriod}: Task(0).wcrt

/*

*/
inf {Task(1).EndPeriod}: Task(1).wcrt

/*

*/
inf {Task(2).EndPeriod}: Task(2).wcrt

/*

*/
inf {Task(3).EndPeriod}: Task(3).wcrt

/*
Check that semaphores are taken by at most one process at a time.
*/
A[] forall(i : sid_t) sum(j : pid_t) Task(j).sema[i] <= 1

/*
Worst-case response times.
*/
sup: Task(0).wcrt , Task(1).wcrt, Task(2).wcrt, Task(3).wcrt

/*
Check that the system is schedulable.
*/
A[] forall(i : pid_t) not Task(i).Error
