diff --git a/src/main.c b/src/main.c index 8a59cd772bd0ccecdc59217100c6ba96f34bdc5e..3621eae32313fd2774c655b3cfd1a78f6a350795 100644 --- a/src/main.c +++ b/src/main.c @@ -1,5 +1,5 @@ //#define KLEE -#define KLEE_WCET +//#define KLEE_WCET #ifdef KLEE #include "SRP_klee.h" @@ -40,7 +40,7 @@ // resource ceilings #define r1_Ceiling 2 -#define r2_Ceiling 1 +#define r2_Ceiling 3 // Analysis variables static volatile int state; @@ -49,7 +49,7 @@ static int job; void work(int i) { volatile int k = 0; - for (int j = 0; j < 100 * i; j++) + for (int j = 0; j < 50 * i; j++) { k++; } @@ -86,16 +86,26 @@ TASK(j2) TRACE("j2_r1_locked\n"); work(5); UNLOCK(r1); + if (state == 100) + { + work(2); + } + else + { + work(1); + } + TRACE("j2_exit\n"); } TASK(j3) { TRACE("j3_enter\n"); - LOCK(r1); - TRACE("j3_r1_locked\n"); + LOCK(r2); + TRACE("j3_r2_locked\n"); + work(1); - UNLOCK(r1); + UNLOCK(r2); JOB_REQUEST(j1); TRACE("j3_exit\n"); }