+++ /dev/null
-/*
- * Models the Pathfinder scheduling algorithm and explains the
- * cause of the recurring reset problem during the mission on Mars
- *
- * there is a high priority process, that consumes
- * data produced by a low priority process.
- * data consumption and production happens under
- * the protection of a mutex lock
- * the mutex lock conflicts with the scheduling priorities
- * which can deadlock the system if high() starts up
- * while low() has the lock set
- * there are 12 reachable states in the full (non-reduced)
- * state space -- two of which are deadlock states
- * partial order reduction cannot be used here because of
- * the 'provided' clause that models the process priorities
- */
-
-mtype = { free, busy, idle, waiting, running };
-
-show mtype h_state = idle;
-show mtype l_state = idle;
-show mtype mutex = free;
-
-active proctype high() /* can run at any time */
-{
-end: do
- :: h_state = waiting;
- atomic { mutex == free -> mutex = busy };
- h_state = running;
-
- /* critical section - consume data */
-
- atomic { h_state = idle; mutex = free }
- od
-}
-
-active proctype low() provided (h_state == idle) /* scheduling rule */
-{
-end: do
- :: l_state = waiting;
- atomic { mutex == free -> mutex = busy};
- l_state = running;
-
- /* critical section - produce data */
-
- atomic { l_state = idle; mutex = free }
- od
-
-}
-