Skip to content
Snippets Groups Projects
Commit 63e74303 authored by pln's avatar pln
Browse files

added additional condition

parent d8f29ea3
Branches
No related tags found
No related merge requests found
//#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");
}
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment