Commit 888c28a0 authored by Erwan Jahier's avatar Erwan Jahier
Browse files

Clean-up the git repo by updating the .gitignore + adding missing stuff

Also extend the Data module so that it can be shared with lus2lic.
parent 000eb377
......@@ -45,6 +45,7 @@ objs
*.bak
*.save
*.res
*.exp
*.exp-ocaml7
*luc
*.ec
......@@ -57,6 +58,8 @@ objs
*.di
*.c
*.h
*.rzi
*.iso
*.dot
*.top
source/mli_save
......@@ -189,4 +192,23 @@ mymakefile
examples/lutin/catherine
examples/lutin/simplice
examples/lutin/chaouki
*.annot
\ No newline at end of file
*.annot
*.out
VALORISATION
examples/*/*/*.*.*/
examples/*/*/*/*.*.*/
.nfs*
poubelle
source/Lurettetop/ldbg.org
examples/rml/window.ml
install/ldbg
install/xlurette.bat
install/set_env_var.bat
*.cov
*.dump
examples/lutin/no-input/
examples/lutin/socket-from-ocaml/call-via-socket
examples/lutin/socket-from-ocaml/lutin
examples/lutin/adacs/
examples/lutin/alice/
examples/lutin/comon/
open Event;;
open Ldbg;;
open Ldbg_utils;;
add_rp "sut:ocaml:rabbit.cmxs:";;
add_rp "env:lutin:rabbit.lut:-main:rabbit:-L:libm.so:-loc";;
stl 100;;
set_sim2chro false;;
set_gnuplot false;;
let rec n e i =
if i = 0 then (print e; e)
else
let e = next e in
if !show_trace then print e;
n e (i-1);;
-- incremente le compteur si b
node incr_cond(cpt:int; c:bool) returns (n_cpt:int);
let
n_cpt = cpt + if c then 1 else 0;
tel;
node compte__m<<const m:int>>(tab : bool^m)
returns (ok:bool);
let
ok = (red<<incr_cond, m>>(0, tab) <= n);
tel;
node bool_utils_au_plus_2_parmi_3 = au_plus_n_parmi_m<<2,3>>;
extern bool_utils_au_plus_2_parmi_3(b1, b2, b3:bool): bool
node au_plus_2_parmi_3(b1, b2, b3:bool) returns (ok:bool) =
loop
ok = bool_utils_au_plus_2_parmi_3(b1, b2, b3)
\ No newline at end of file
let min(x, y : real) : real = if x < y then x else y
let max(x, y : real) : real = if x > y then x else y
-- Always loop, even if t deadlocks
let myloop(t:trace) : trace = loop try loop t
-- We flag it as valid after delay consecutive cycles without reset.
-- We reset as soon as diff > epsilon.
node is_d_epsilon_stable(d:int; epsilon, v: real) returns (res:bool) =
exist vmin, vmax, diff : real in
let init() = (vmin = v) and (vmax = v) and (diff = 0.0) and not res in
let step() = vmin = min(v, pre vmin) and vmax = max(v, pre vmax) and
diff = ((vmax - vmin) / 2.0)
in
myloop (
init() fby
assert step() and diff <= epsilon in
loop [d] not res fby
loop res
)
node is_d_m_epsilon_stable(d, m:int ; epsilon, v:real) returns (res:bool) =
exist stable : bool in
run stable := is_d_epsilon_stable(d, epsilon, v) in
myloop (
loop { not stable and not res } fby
loop [m] { stable and not res } fby
strong loop { stable and res }
)
node is_stable(v:real) returns (res:bool) =
run res := is_d_m_epsilon_stable(3, 5, 3.0, v)
-- ca sert à rien le is_d_m_epsilon_stable comparé au is_d_epsilon_stable
-- il suffit de prendre d+m et ca fait la meme chose...
--
-- un truc plus interessant, serait de coder un is_3_epsilon_stable exacte,
-- et de l'utiliser dans is_stable
-- exact, and expensive (but for m=3 its ok)
node is_3_stable(epsilon, v:real) returns (vref:real;res:bool) =
exist v1,v2,v3 : real in
v1 = v and v2 = v and v3 = v and not res and vref = v
fby
assert v1 = v and v2 = pre v1 and v3 = pre v2 and vref = (v1+v2+v3)/3.0 in
loop [2] not res
fby
loop {
res = abs(v1-v2)<epsilon and
abs(v1-v3)<epsilon and
abs(v2-v3)<epsilon
}
-- this one is an abstraction
node is_m_stable(d, m:int ; epsilon, v:real) returns (res:bool) =
exist v_average : real in
exist vref : real in
exist is_3_stable : bool in
run v_average, is_3_stable := is_3_stable(epsilon,v) in
myloop (
loop not is_3_stable and not res and vref = v_average
fby
-- on se souvient de la valeur de ref à l'entree de ce loop pour
-- détecter une lente dérive de v.
assert
is_3_stable and -- as soon it is false, we start from the beginning
vref = pre vref and
abs(v-vref) < epsilon -- will detect drift
in
loop [m] not res fby
loop res
)
\ No newline at end of file
let between(x, min, max : real) : bool = ((min < x) and (x < max))
let cross_product(ux,uy,vx,vy:real) : real = (ux*vy-uy*vx)
let is_inside(px,py,p1x,p1y,p2x,p2y,p3x,p3y,p4x,p4y : real) : bool =
let p1p_x = px-p1x in
let p1p_y = py-p1y in
let p2p_x = px-p2x in
let p2p_y = py-p2y in
let p3p_x = px-p3x in
let p3p_y = py-p3y in
let p4p_x = px-p4x in
let p4p_y = py-p4y in
let p2p1_x = p1x-p2x in
let p2p1_y = p1y-p2y in
let p1p4_x = p4x-p1x in
let p1p4_y = p4y-p1y in
let p4p3_x = p3x-p4x in
let p4p3_y = p3y-p4y in
let p3p2_x = p2x-p3x in
let p3p2_y = p2y-p3y in
cross_product(p2p1_x, p2p1_y, p2p_x, p2p_y) >= 0.0 and -- p2p1 ^ p2p < 0
cross_product(p1p4_x, p1p4_y, p1p_x, p1p_y) >= 0.0 and -- p1p4 ^ p1p < 0
cross_product(p4p3_x, p4p3_y, p4p_x, p4p_y) >= 0.0 and -- p4p3 ^ p4p < 0
cross_product(p3p2_x, p3p2_y, p3p_x, p3p_y) >= 0.0 -- p3p2 ^ p3p < 0
let delta = 5.0
-- p1
-- (0,ymax)---------------------(xmax,ymax)
-- | |
-- | |
-- | |
-- | |
-- | |
-- | |
-- | | p2
-- | p4 |
-- | |
-- | |
-- | |
-- | |
-- | |
-- | |
-- | |
-- | |
-- (0,0)----------------------------(xmax,0)
-- p3
-- let cross_product(ux,uy,vx,vy:real) : real = (ux*vy-uy*vx)
-- p est à droite du vecteur p1p2 ssi p1p2 ^ p1p < 0.0
let adroite(px,py,p1x,p1y,p2x,p2y:real) =
cross_product(p2x-p1x, p2y-p1y, px-p1x, py-p1y) < 0.0
node ivrogne (p1, p2, p3, p4 : real; -- pourcentage
x_min, x_max, y_min, y_max : real)
returns(x, y: real) =
let p1x:real = p1*x_max/100. in
let p1y:real = y_max in
let p2x:real = x_max in
let p2y:real = p2*y_max/100. in
let p3x:real = p3*x_max/100.in
let p3y:real = y_min in
let p4x:real = x_min in
let p4y:real = p4*y_max/100. in
let cstr() =
is_inside(x,y, p1x, p1y, p2x, p2y, p3x, p3y, p4x, p4y)
in
{ cstr() |> x = 2. and y = 2. }
fby
loop {
cstr() and
between(x, pre x - delta, pre x + delta) and
between(y, pre y - delta, pre y + delta)
|>
cstr()
}
node idiot (t:bool) returns(x,y:real) =
assert x = 10. in
run x,y := ivrogne(20., 20., 20., 20., 0., 100., 0., 200.)
\ No newline at end of file
LTOP=../../../bin/lurettetop
LDBG=../../../bin/ldbg
EXPDIR=`$(LTOP) --ocaml-version`
$(EXPDIR):
[ -d $(EXPDIR) ] || (mkdir -p $(EXPDIR) ; make utest)
# step forward
test1.rif: $(EXPDIR)
rm -f test1.rif0
$(LDBG) -init test.ml > test1.rif0
grep -v "lurette chronogram" test1.rif0 | \
grep -v "This is ldbg Version" test1.rif0 | \
sed -e "s/^M//" > test1.rif
test1: test1.rif $(EXPDIR)
rm -f test1.res
diff -B -u -i $(EXPDIR)/test1.rif.exp test1.rif > test1.res || true
cat test1.res
[ ! -s test1.res ] && make clean
utest1:test1.rif
cp test1.rif $(EXPDIR)/test1.rif.exp
# use profiler
test2.rif: $(EXPDIR)
rm -f test2.rif0
$(LDBG) -init test2.ml > test2.rif0
grep -v "lurette chronogram" test2.rif0 | \
grep -v "This is ldbg Version" test2.rif0 | \
sed -e "s/^M//" > test2.rif
test2: test2.rif $(EXPDIR)
rm -f test2.res
diff -B -u -i $(EXPDIR)/test2.rif.exp test2.rif > test2.res || true
cat test2.res
[ ! -s test2.res ] && make clean
utest2:test2.rif
cp test2.rif $(EXPDIR)/test2.rif.exp
# check the slides demo
test3.rif: $(EXPDIR)
rm -f test3.rif0
$(LDBG) -init test3.ml > test3.rif0
grep -v "lurette chronogram" test3.rif0 | \
grep -v "This is ldbg Version" test3.rif0 | \
sed -e "s/^M//" > test3.rif
test3: test3.rif $(EXPDIR)
rm -f test3.res
diff -B -u -i $(EXPDIR)/test3.rif.exp test3.rif > test3.res || true
cat test3.res
[ ! -s test3.res ] && make clean
utest3:test3.rif
cp test3.rif $(EXPDIR)/test3.rif.exp
# check the slides demo
test5.rif: $(EXPDIR)
rm -f test5.rif0
$(LDBG) -init test5.ml > test5.rif0
grep -v "lurette chronogram" test5.rif0 | \
grep -v "This is ldbg Version" test5.rif0 | \
sed -e "s/^M//" > test5.rif
test5: test5.rif $(EXPDIR)
rm -f test5.res
diff -B -u -i $(EXPDIR)/test5.rif.exp test5.rif > test5.res || true
cat test5.res
[ ! -s test5.res ] && make clean
utest5:test5.rif
cp test5.rif $(EXPDIR)/test5.rif.exp
utest: utest1 utest2 utest3 utest5
test: test1 test2 test3 test5 clean
%.ec: %.lus
clean:
rm -rf *.h *.c *.ec *.log *~ .*~ *.o *rif0 *rif Data *.pp_luc *.plot *.gp *.cov *.cm* *.dro
open Event;
open Ldbg;;
open Ldbg_utils;;
set_sim2chro false;;
(* set_gnuplot false;; *)
ltop "set_seed 1";;
add_rp "env:lutin:ex1.lut:main2" ;;
stl 100;;
let e = run ();;
let e = nexti e 500;;
let e = step e ;;
let e = nexti e 500;;
e.terminate();;
(*
break "ex1.lut::34" ;;
let e = continue e;;
*)
Lurette entities (SUT, oracles, environments) can also be a
stand-alone program that reads and writes its inputs/outputs on a
socket. Of course, such programs ougth to respect a precise protocol
that we describe below.
- First it must *connect to an inet socket* (defined by an address and
a port), using the ~listen~ command;
- Then it must write its *input variable names and types* (that will be
received from the lurette process) using the [[RIF]] convention
- Then it must write its *output variable names and types* (that will be
send to lurette process) using the [[RIF]] convention
- Then, it enter a loop where it
+ reads its input on the socket (in their declaration order)
+ writes its output on the socket (in their declaration order)
In order to stop that loop and inform lurette it wants to stop
playing, the program just have to send the ~#quit~ command.
Here a small but complete example of a C program that is able to
communicate with Lurette (and that is part of its non-regression test
suite) :
file:simple_sut.c
#
# Illustrate the use of a ocaml programs that calls the lutin interpreter
# via sockets
################################################################
MAIN=call_foo_via_socket
$(MAIN):$(MAIN).c
ifeq ($(HOSTTYPE),cross-win32)
$(CC) $(MAIN).c -o $(MAIN) -D_WIN32 -D_WINSOCK -lws2_32
else ifeq ($(HOSTTYPE),win32)
$(CC) -mno-cygwin $(MAIN).c -o $(MAIN) -D_WIN32 -D_WINSOCK -lws2_32
else ifeq ($(HOSTTYPE),cygwin)
$(CC) $(MAIN).c -o $(MAIN) -D_WIN32
else
$(CC) $(MAIN).c -o $(MAIN)
endif
################################################################
clean:
rm -f *.0 *~ $(MAIN) *~ *.rif test.res
do: $(MAIN)
cp $(MAIN) $(MAIN).exe
test: clean $(MAIN)
./$(MAIN)
cat $(MAIN).rif | sed -e "s/^M//" > $(MAIN)-2.rif
rm -f test.res && diff -B -u -w -i $(MAIN).rif.exp $(MAIN)-2.rif > test.res && \
[ ! -s test.res ] && make clean
utest:
cp $(MAIN).rif $(MAIN).rif.exp
#include <stdio.h>
#include <sys/types.h>
#ifdef _WIN32
#include <process.h>
#endif
#ifdef _WINSOCK
#include <windows.h>
#include <winsock2.h>
#include <stdio.h>
#pragma comment(lib, "ws2_32.lib")
#else
#include <sys/socket.h>
#include <netinet/in.h>
#include <netdb.h>
#include <string.h>
#endif
// Demonstrate the use of a ocaml programs that calls the lutin interpreter via sockets.
#define MAX_BUFF_SIZE 256
int main()
{
int lutin_pid,sockfd, newsockfd, portno, clilen, i,n;
FILE *rif;
struct sockaddr_in serv_addr, cli_addr;
char buffer[MAX_BUFF_SIZE];
char portno_str[10];
#ifdef _WINSOCK
WSADATA WSAData;
WSAStartup(MAKEWORD(2,0), &WSAData);
#endif
printf("Starting...\n");
rif=fopen("call_foo_via_socket.rif", "w");
// Socket administration stuff
sockfd = socket(AF_INET, SOCK_STREAM, 0);
if (sockfd < 0) error("opening socket");
serv_addr.sin_family = AF_INET;
// serv_addr.sin_addr.s_addr = ((struct in_addr *)(my_entrie_byname->h_addr))->s_addr;
serv_addr.sin_addr.s_addr = inet_addr("127.0.0.1");
printf("Binding...\n");
portno = 2000;
serv_addr.sin_port = htons(portno);
while (bind(sockfd, (struct sockaddr *) &serv_addr, sizeof(serv_addr)) ) {
portno++;
serv_addr.sin_port = htons(portno);
};
//itoa(portno, portno_str,10);
sprintf(portno_str, "%d", portno);
printf("Forking...%i %s\n",portno,portno_str);
const char *args[] = {
"call-via-socket", "127.0.0.1", portno_str, "lutin", "-seed","42", "foo.lut", "-rif","foo.rif",
// "-l", "10",
// "-vl","1",
NULL};
#ifdef _WIN32
_spawnvp(_P_DETACH, args[0], args);
#else
lutin_pid = fork();
if(lutin_pid == 0) {
execvp(args[0], args);
printf("Unknown command\n");
return 0;
}
#endif
printf("Listening...\n");
listen(sockfd,5);
clilen = sizeof(cli_addr);
printf("Accepting...\n");
newsockfd = accept(sockfd, (struct sockaddr *) &cli_addr, &clilen);
if (newsockfd < 0) error(" on accept");
// read the first two lines
printf("Reading...(%s)\n",buffer);
readnf(newsockfd,buffer);
fprintf(rif, "%s\n",buffer);
readnf(newsockfd,buffer);
fprintf(rif, " %s\n",buffer);
int j, rc;
int a;
char b;
float c;
// ok, let's loop with the lutin process
for(i=0; i < 100; i++) {
printf("Looping...%d\n",i);
send(newsockfd,"42 t 3.14\n",10,0);
//readnf(newsockfd,buffer); // step number
//readnf(newsockfd,buffer); // outs
bzero(buffer,MAX_BUFF_SIZE);
rc = 0;
while (1) {
rc = recv(newsockfd, buffer, MAX_BUFF_SIZE, 0);
if (rc > 0) break;
}
sscanf(buffer,"#step %d #outs %d %c %f ",&j, &a, &b, &c);
fprintf(rif, "#step %d \n42 t 3.14 #outs %d %c %f\n",j,a,b,c);
}
printf("Exiting...\n");
write(newsockfd,"q\n",2);
close(sockfd);
close(newsockfd);
fclose(rif);
#ifdef _WINSOCK
WSACleanup();
#endif
return 0;
}
int error(int n, char *msg)
{
printf("Error %s",msg);
return n;
}
/**
* readnf() - reading from a file descriptor but a bit smarter
**/
int readnf (int fd, char *line)
{
if (readline(fd, line, MAX_BUFF_SIZE) < 0) return 2;
return 0;
}
/**
* readline() - read an entire line from a file descriptor until a newline.
* functions returns the number of characters read but not including the
* null character.
**/
int readline(int fd, char *str, int maxlen)
{
int n; /* no. of chars */
int readcount; /* no. characters read */
char c='a';
for (n = 1; n < maxlen; n++) {
/* read 1 character at a time */
//readcount = read(fd, &c, 1); /* store result in readcount */
readcount = recv(fd, &c, 1, 0);
// printf("Reading char %c (%i)\n",c,readcount);