diff --git a/examples/random/README b/examples/random/README new file mode 100644 index 0000000..93f83d2 --- /dev/null +++ b/examples/random/README @@ -0,0 +1,21 @@ +Simple Markov chain simulation by external call to random() C function : + +- random.epi : Heptagon interface containing the declaration of + random() function + +- random.h, random.c : "glue" between actual random() C function and + function calls generated by Heptagon + +- markov.ept : contains node "process", simulating a two-state Markov + chain, with probability p (constant) at each step to go from one + state to the other + +Function "random" and node "process" are declared unsafe to avoid +optimization removing calls to "random" ("random" has side effects). + +Compilation and simulation : + +heptc random.epi +heptc -target c -s process -hepts markov.ept +gcc -I . -I markov_c -I /usr/local/lib/heptagon/c random.c markov_c/_main.c markov_c/markov.c markov_c/markov_types.c -o markov +hepts -mod Markov -node process -exec ./markov diff --git a/examples/random/markov.ept b/examples/random/markov.ept new file mode 100644 index 0000000..59c2cb0 --- /dev/null +++ b/examples/random/markov.ept @@ -0,0 +1,20 @@ +open Random + +const p : float = 0.3 + +unsafe node process() = (o:bool) +let + automaton + state A + var c : bool; + do o = false; c = random() <. p; + until c then B + | not c then C + state B + var c : bool; + do o = true; c = random() <. p + until c then A + state C + do o = false + end +tel diff --git a/examples/random/mathext.c b/examples/random/mathext.c new file mode 100644 index 0000000..5a7b302 --- /dev/null +++ b/examples/random/mathext.c @@ -0,0 +1,15 @@ + +#include +#include "mathext.h" + +void Mathext__power_step(float x, int n, Mathext__power_out *o) { + float r; + int i; + + r = 1.0; + for (i = 1; i <= n; i++) { + r = r * x; + } + o->y = r; +} + diff --git a/examples/random/mathext.epi b/examples/random/mathext.epi new file mode 100644 index 0000000..f267c91 --- /dev/null +++ b/examples/random/mathext.epi @@ -0,0 +1,3 @@ + +(* output : y = x^n *) +val fun power(x:float; n:int) = (y:float) diff --git a/examples/random/mathext.h b/examples/random/mathext.h new file mode 100644 index 0000000..04ee8be --- /dev/null +++ b/examples/random/mathext.h @@ -0,0 +1,14 @@ + +#ifndef MATHEXT_H +#define MATHEXT_H + + +/* Example of a combinatorial function */ +typedef struct Mathext__power_out { + float y; +} Mathext__power_out; + +void Mathext__power_step(float x, int n, Mathext__power_out *o); + +#endif + diff --git a/examples/random/random.c b/examples/random/random.c new file mode 100644 index 0000000..5d8a4b4 --- /dev/null +++ b/examples/random/random.c @@ -0,0 +1,8 @@ + +#include +#include "random.h" + +void Random__random_step(Random__random_out *o) { + o->z = ((double)random())/((double)RAND_MAX); +} + diff --git a/examples/random/random.epi b/examples/random/random.epi new file mode 100644 index 0000000..b0e03e4 --- /dev/null +++ b/examples/random/random.epi @@ -0,0 +1,3 @@ + +(* output : random float in interval [0,1] *) +unsafe val fun random() = (z:float) diff --git a/examples/random/random.h b/examples/random/random.h new file mode 100644 index 0000000..3e17aea --- /dev/null +++ b/examples/random/random.h @@ -0,0 +1,14 @@ + +#ifndef RANDOM_H +#define RANDOM_H + + +/* Example of a combinatorial function */ +typedef struct Random__random_out { + float z; +} Random__random_out; + +void Random__random_step(Random__random_out *o); + +#endif +