Skip to content
Snippets Groups Projects
Commit 1f305471 authored by Henrik Tjäder's avatar Henrik Tjäder
Browse files

Merge branch 'klee' of gitlab.henriktjader.com:d7020e/d7020e_srp into klee

parents 020e9783 63e74303
No related branches found
No related tags found
No related merge requests found
//#define KLEE //#define KLEE
#define KLEE_WCET //#define KLEE_WCET
#ifdef KLEE #ifdef KLEE
#include "SRP_klee.h" #include "SRP_klee.h"
...@@ -40,7 +40,7 @@ ...@@ -40,7 +40,7 @@
// resource ceilings // resource ceilings
#define r1_Ceiling 2 #define r1_Ceiling 2
#define r2_Ceiling 1 #define r2_Ceiling 3
// Analysis variables // Analysis variables
static volatile int state; static volatile int state;
...@@ -49,7 +49,7 @@ static int job; ...@@ -49,7 +49,7 @@ static int job;
void work(int i) void work(int i)
{ {
volatile int k = 0; volatile int k = 0;
for (int j = 0; j < 100 * i; j++) for (int j = 0; j < 50 * i; j++)
{ {
k++; k++;
} }
...@@ -86,16 +86,26 @@ TASK(j2) ...@@ -86,16 +86,26 @@ TASK(j2)
TRACE("j2_r1_locked\n"); TRACE("j2_r1_locked\n");
work(5); work(5);
UNLOCK(r1); UNLOCK(r1);
if (state == 100)
{
work(2);
}
else
{
work(1);
}
TRACE("j2_exit\n"); TRACE("j2_exit\n");
} }
TASK(j3) TASK(j3)
{ {
TRACE("j3_enter\n"); TRACE("j3_enter\n");
LOCK(r1); LOCK(r2);
TRACE("j3_r1_locked\n"); TRACE("j3_r2_locked\n");
work(1); work(1);
UNLOCK(r1); UNLOCK(r2);
JOB_REQUEST(j1); JOB_REQUEST(j1);
TRACE("j3_exit\n"); TRACE("j3_exit\n");
} }
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment