Commit 5ff210d0 authored by erwan's avatar erwan

remove untested examples

parent f0b2e7c5
Pipeline #18235 passed with stages
in 8 minutes and 40 seconds
OASISFormat: 0.4
Name: lutin
Version: 2.65
Version: 2.66
Authors: Erwan Jahier, Pascal Raymond, Bertrand Jeannnet (polka), Yvan Roux
Maintainers: erwan.jahier@univ-grenoble-alpes.fr
License: CeCILL
......
This directory contains examples that are not tracked by the test
scripts, which means that some (most) programs might not (even) be
syntactically correct (anymore).
let CYCLE_LUTIN = 250
let deux_vrai(p1, p2: bool): bool = {
p1 and p2
}
let trois_vrai(p1, p2, p3, p4: bool): bool = {
(p1 and p2 and p3)
or (p1 and p2 and p4)
or (p1 and p3 and p4)
or (p2 and p3 and p4)
}
let casser_au_moins_1_et_au_plus_2_sur_4(p1, p2, p3, p4: bool): bool = {
((p1 or p2) and (not p3) and (not p4))
or ((p1 or p3) and (not p2) and (not p4))
or ((p1 or p4) and (not p2) and (not p3))
or ((p2 or p3) and (not p1) and (not p4))
or ((p2 or p4) and (not p1) and (not p3))
or ((p3 or p4) and (not p1) and (not p2))
}
let casser_1_sur_2(p1, p2: bool): bool = {
(p1 and not p2) or (not p1 and p2)
}
let Max(x, y: int): int = {
if x < y then y else x
}
-- Prend le temps en ms
let loop_time(n: int): trace = {
exist cpt: int = n in
loop {
cpt = Max(0, pre cpt - CYCLE_LUTIN) and cpt <> 0
}
}
let loop_time_reset(n: int; reset: bool): trace = {
exist cpt: int = n in
loop {
(cpt = Max(0, pre cpt - CYCLE_LUTIN)) and (cpt <> 0) and not reset
}
}
node nominal() returns (EXE101MN_Panne2_OnOff: bool;
EXE101MN_Panne2_Valeur: real;
EXE102MN_Panne2_OnOff: bool;
EXE102MN_Panne2_Valeur: real;
EXE103MN_Panne2_OnOff: bool;
EXE103MN_Panne2_Valeur: real;
EXE104MN_Panne2_OnOff: bool;
EXE104MN_Panne2_Valeur: real;
EXE701PO_Panne1_OnOff: bool;
EXE702PO_Panne1_OnOff: bool) =
let Nominal = (EXE101MN_Panne2_OnOff = false) and
(EXE101MN_Panne2_Valeur = 0.0) and
(EXE102MN_Panne2_OnOff = false) and
(EXE102MN_Panne2_Valeur = 0.0) and
(EXE103MN_Panne2_OnOff = false) and
(EXE103MN_Panne2_Valeur = 0.0 ) and
(EXE104MN_Panne2_OnOff = false) and
(EXE104MN_Panne2_Valeur = 0.0) and
(EXE701PO_Panne1_OnOff = false) and
(EXE702PO_Panne1_OnOff = false)
in
loop Nominal
node pannes_interactif(n:int; reset: bool) returns (
EXE101MN_Panne2_OnOff: bool;
EXE101MN_Panne2_Valeur: real [0.0; 30.0];
EXE102MN_Panne2_OnOff: bool;
EXE102MN_Panne2_Valeur: real [0.0; 30.0];
EXE103MN_Panne2_OnOff: bool;
EXE103MN_Panne2_Valeur: real [0.0; 30.0];
EXE104MN_Panne2_OnOff: bool;
EXE104MN_Panne2_Valeur: real [0.0; 30.0];
EXE701PO_Panne1_OnOff: bool;
EXE702PO_Panne1_OnOff: bool;
Urgence: bool) =
let nb_pannes =
(if EXE101MN_Panne2_Valeur > 0.0 then 1 else 0) +
(if EXE102MN_Panne2_Valeur > 0.0 then 1 else 0) +
(if EXE103MN_Panne2_Valeur > 0.0 then 1 else 0) +
(if EXE104MN_Panne2_Valeur > 0.0 then 1 else 0) +
(if EXE101MN_Panne2_OnOff then 1 else 0) +
(if EXE102MN_Panne2_OnOff then 1 else 0) +
(if EXE103MN_Panne2_OnOff then 1 else 0) +
(if EXE104MN_Panne2_OnOff then 1 else 0) +
(if EXE701PO_Panne1_OnOff then 1 else 0) +
(if EXE702PO_Panne1_OnOff then 1 else 0)
in
let bouge_pas = (EXE101MN_Panne2_OnOff = pre EXE101MN_Panne2_OnOff) and
(EXE101MN_Panne2_Valeur = pre EXE101MN_Panne2_Valeur) and
(EXE102MN_Panne2_OnOff = pre EXE102MN_Panne2_OnOff) and
(EXE102MN_Panne2_Valeur = pre EXE102MN_Panne2_Valeur) and
(EXE103MN_Panne2_OnOff = pre EXE103MN_Panne2_OnOff) and
(EXE103MN_Panne2_Valeur = pre EXE103MN_Panne2_Valeur) and
(EXE104MN_Panne2_OnOff = pre EXE104MN_Panne2_OnOff) and
(EXE104MN_Panne2_Valeur = pre EXE104MN_Panne2_Valeur) and
(EXE701PO_Panne1_OnOff = pre EXE701PO_Panne1_OnOff) and
(EXE702PO_Panne1_OnOff = pre EXE702PO_Panne1_OnOff)
in
let urgence = deux_vrai(EXE701PO_Panne1_OnOff, EXE702PO_Panne1_OnOff)
or
trois_vrai(
EXE101MN_Panne2_OnOff,
EXE102MN_Panne2_OnOff,
EXE103MN_Panne2_OnOff,
EXE104MN_Panne2_OnOff)
or
trois_vrai(
EXE101MN_Panne2_Valeur > 0.0,
EXE102MN_Panne2_Valeur > 0.0,
EXE103MN_Panne2_Valeur > 0.0,
EXE104MN_Panne2_Valeur > 0.0)
in
assert EXE101MN_Panne2_Valeur = 0.0 or EXE101MN_Panne2_Valeur > 0.0 in
assert EXE102MN_Panne2_Valeur = 0.0 or EXE102MN_Panne2_Valeur > 0.0 in
assert EXE103MN_Panne2_Valeur = 0.0 or EXE103MN_Panne2_Valeur > 0.0 in
assert EXE104MN_Panne2_Valeur = 0.0 or EXE104MN_Panne2_Valeur > 0.0 in
-- XXX si je déplie la def de urgence ici, ca na se comporte pas pareil !!!
-- Plus précisément, Urgence ne passe jamais a faux
-- c'est un pb de parenthesage ! la priorité du = est contre-intuitive... la changer ?
assert
Urgence = (
deux_vrai(EXE701PO_Panne1_OnOff, EXE702PO_Panne1_OnOff)
or
trois_vrai(
EXE101MN_Panne2_OnOff,
EXE102MN_Panne2_OnOff,
EXE103MN_Panne2_OnOff,
EXE104MN_Panne2_OnOff)
or
trois_vrai(
EXE101MN_Panne2_Valeur > 0.0,
EXE102MN_Panne2_Valeur > 0.0,
EXE103MN_Panne2_Valeur > 0.0,
EXE104MN_Panne2_Valeur > 0.0)
)
in
-- assert Urgence = urgence in
loop {
loop {
(not Urgence and (nb_pannes = n)) fby
assert bouge_pas in loop_time_reset(7000, reset)
}
|> nb_pannes = n
|> nb_pannes = 10
}
node pannes() returns (EXE101MN_Panne2_OnOff: bool;
EXE101MN_Panne2_Valeur: real [0.0; 30.0];
EXE102MN_Panne2_OnOff: bool;
EXE102MN_Panne2_Valeur: real [0.0; 30.0];
EXE103MN_Panne2_OnOff: bool;
EXE103MN_Panne2_Valeur: real [0.0; 30.0];
EXE104MN_Panne2_OnOff: bool;
EXE104MN_Panne2_Valeur: real [0.0; 30.0];
EXE701PO_Panne1_OnOff: bool;
EXE702PO_Panne1_OnOff: bool) = {
let Urgence = deux_vrai(EXE701PO_Panne1_OnOff, EXE702PO_Panne1_OnOff)
or
trois_vrai(
EXE101MN_Panne2_OnOff,
EXE102MN_Panne2_OnOff,
EXE103MN_Panne2_OnOff,
EXE104MN_Panne2_OnOff)
in
let bouge_pas = (EXE101MN_Panne2_OnOff = pre EXE101MN_Panne2_OnOff) and
(EXE101MN_Panne2_Valeur = pre EXE101MN_Panne2_Valeur) and
(EXE102MN_Panne2_OnOff = pre EXE102MN_Panne2_OnOff) and
(EXE102MN_Panne2_Valeur = pre EXE102MN_Panne2_Valeur) and
(EXE103MN_Panne2_OnOff = pre EXE103MN_Panne2_OnOff) and
(EXE103MN_Panne2_Valeur = pre EXE103MN_Panne2_Valeur) and
(EXE104MN_Panne2_OnOff = pre EXE104MN_Panne2_OnOff) and
(EXE104MN_Panne2_Valeur = pre EXE104MN_Panne2_Valeur) and
(EXE701PO_Panne1_OnOff = pre EXE701PO_Panne1_OnOff) and
(EXE702PO_Panne1_OnOff = pre EXE702PO_Panne1_OnOff)
in
assert EXE101MN_Panne2_Valeur = 0.0 or EXE101MN_Panne2_Valeur > 0.0 in
assert EXE102MN_Panne2_Valeur = 0.0 or EXE102MN_Panne2_Valeur > 0.0 in
assert EXE103MN_Panne2_Valeur = 0.0 or EXE103MN_Panne2_Valeur > 0.0 in
assert EXE104MN_Panne2_Valeur = 0.0 or EXE104MN_Panne2_Valeur > 0.0 in
loop{
not Urgence fby
assert bouge_pas in loop_time(7000)
}
}
\ No newline at end of file
node toto(x: real) returns (y:real) = {
exist prex: real = x in
y = prex
}
\ No newline at end of file
node n (i:bool) returns(x: real) =
loop ~5: 1 { i and x=42. }
\ No newline at end of file
node between(min, max : real) returns (x:real) =
loop ((min < x) and (x < max))
node n ()
returns(x, y: real) =
-- Si j'interverti les 2 lignes suivantes, ca marche, mais bon,
-- il me semble que x devrait etre sustitué dans les macros également
let macro() = x * y > 0.0 in
run x:= between(-42., 42.0) in
loop { macro() }
\ No newline at end of file
#inputs "a":int "b":bool "c":real
#outputs "x":int "y":bool "z":real
# step 0
10 0 20.000000 #outs 0 1 0.000000
# step 1
10 0 20.000000 #outs 6 1 16.571847
# step 2
10 0 20.000000 #outs 14 0 19.036049
# step 3
10 0 20.000000 #outs 6 0 22.087270
# step 4
10 0 20.000000 #outs 8 0 20.600566
# step 5
10 0 20.000000 #outs 11 1 24.566902
# step 6
10 0 20.000000 #outs 10 1 18.532594
# step 7
10 0 20.000000 #outs 7 1 23.330752
# step 8
10 0 20.000000 #outs 8 0 21.544592
# step 9
10 0 20.000000 #outs 13 1 16.263999
LINKER= $(CC)
EXE=
DEBUG=
DEBUG=-D_DEBUG
CFLAGS = \
-L../../../lib \
-I../../../include -L$(shell ocamlc -where) \
-L$(shell ocamlc -where)/../lutin \
-I$(shell ocamlc -where)/../lutin \
-L../../../_build/lutin/src \
$(DEBUG)
LIBS = lut4c.a liblut4c_stubs.a -lgmp -lm -ldl -lstdc++
LIBS = ../../../_build/lutin/src/lut4c.a ../../../_build/lutin/src/liblut4c_stubs.a \
-lasmrun -lgmp -lm -ldl
LIBS = ../../../_build/lutin/src/lut4c.a ../../../_build/lutin/src/lutin.a -lgmp -lm -ldl -lstdc++
#gcc -o test -L. -L"`ocamlc -where`" test.c -Wl,--whole-archive -lhello_world -Wl,--no-whole-archive -lasmrun -lm -ldl
# -lcamlrun
LUT2C=../../../bin/lutin$(EXE) --2c-4c -seed 42
LUT2CSOCK=../../../bin/lutin$(EXE) --2c-4c-socks 127.0.0.1 -seed 42
CALLVIASOCKET=../../../bin/call-via-socket -addr 127.0.0.1 -port 2004
LUTIN=../../../bin/lutin$(EXE) -seed 42 -only-outputs
ifeq ($(HOSTTYPE),mac)
LINKER=g++ -g
LIBS = -lluc4c_nc -llucky_nc -lgmp -lm -ldl
endif
ifneq (,$(findstring win32,$(HOSTTYPE)))
EXE=.exe
LINKER=$(CC)
CFLAGS = \
-L../../../lib \
-I../../../include -D_WIN32 -D_WINSOCK $(DEBUG) \
-Winline -Wimplicit-function-declaration
LIBS = -lluc4c_nc -llucky_nc -lgmp -lws2_32 -lm -lstdc++ -lole32
LIBSSOCK = -lws2_32 -lole32
LUT2C=../../../bin/lutin.exe --2c-4c
LUT2CSOCK=../../../bin/lutin.exe --2c-4c-socks 127.0.0.1 -seed 42
endif
ifeq ($(HOSTTYPE),cygwin)
EXE=.exe
CFLAGS = \
-L../../../lib \
-I../../../include \
-Winline -Wimplicit-function-declaration
LIBS = -lluc4c_nc -llucky_nc -lgmp -lws2_32 -lm -lstdc++
LUT2C=../../../bin/lutin --2c-4c-socks 127.0.0.1 -seed 42
endif
################################################################
# Calling lucky from C
foo.c: foo.lut
$(LUT2C) foo.lut
foo.o : foo.c
$(CC) -c $(CFLAGS) foo.c
call_foo.o: call_foo.c
$(CC) -c $(CFLAGS) call_foo.c
foo$(EXE): foo.o call_foo.o
$(LINKER) $(CFLAGS) -o $@ $^ $(LIBS)
################################################################
# Calling lucky from C via sockets
call_foo_sock.o: call_foo_sock.c
$(CC) -c $(CFLAGS) call_foo_sock.c
sock:
$(LUT2CSOCK) foo.lut
make foo.o
foo-sock$(EXE): sock foo.o call_foo_sock.o
$(LINKER) $(CFLAGS) -o $@ foo.o call_foo_sock.o $(LIBSSOCK)
################################################################x
clean:
rm -f run *.o *~ foo foo-sock foo*.h foo*.c foo-sock.c *.gp *.plot *.rif *.log
EXPDIR=`$(LUTIN) --ocaml-version`
$(EXPDIR):
[ -d $(EXPDIR) ] || (mkdir -p $(EXPDIR) ; make utest)
test1.rif : clean foo$(EXE) $(EXPDIR)
./foo$(EXE) > test1.rif
test1:test1.rif
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
utest: utest1 utest2
utest1: test1.rif
./foo$(EXE) > test1.rif
cp test1.rif $(EXPDIR)/test1.rif.exp
test2: clean foo-sock$(EXE) $(EXPDIR)
./foo-sock$(EXE) > test2.rif &
$(CALLVIASOCKET) "$(LUTIN) foo.lut"
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:clean foo-sock$(EXE)
./foo-sock$(EXE) > test2.rif &
$(CALLVIASOCKET) "$(LUTIN) foo.lut"
cp test2.rif $(EXPDIR)/test2.rif.exp
test: test1
LTOP=../../../bin/lurettetop
LURETTETOP=$(LTOP) \
--test-length 100 --thick-draw 1 \
--draw-inside 0 --draw-edges 0 --draw-vertices 0 --draw-all-vertices \
--step-mode Inside --local-var --no-sim2chro --seed 3 \
--do-not-show-step
PORT=2001
xxx:
$(LURETTETOP) --dbg -v 3 \
-rp "sut:socket:127.0.0.1:$(PORT)" \
-rp "env:lutin:foo.lut:env"
xxx2:
../../../bin/call-via-socket -addr 127.0.0.1 -port $(PORT) "lutin -m main foo.lut -rif xxx.rif"
xxx3:foo-sock
./foo-sock
#include <stdlib.h>
#include <stdio.h>
#include "foo.h"
// Output procedures
void foo_O_x(foo_ctx* ctx, int v) { ctx->_x = v; };
void foo_O_y(foo_ctx* ctx, int v) { ctx->_y = v; };
void foo_O_z(foo_ctx* ctx, double v) { ctx->_z = v; };
// a little main that calls the foo.lut program
int main(){
int i = 0;
foo_ctx* ctx;
#ifdef _DEBUG
fp = fopen("debug.log", "w");
#endif
ctx = foo_new_ctx(NULL);
// lutin_set_seed(1);
// setting inputs
foo_I_a(ctx, 10);
foo_I_b(ctx, 0);
foo_I_c(ctx, 20.0);
printf("#inputs \"a\":int \"b\":bool \"c\":real\n");
printf("#outputs \"x\":int \"y\":bool \"z\":real\n");
for (i=0; i<10; i++){
foo_step(ctx, step_inside);
printf("# step %d \n%d %d %f #outs %d %d %f\n",
i, ctx->_a, ctx->_b, ctx->_c, ctx->_x, ctx->_y, ctx->_z);
}
return 0;
}
#include <stdlib.h>
#include <stdio.h>
#include "foo.h"
// Output procedures
void foo_O_x(foo_ctx* ctx, _int v) { ctx->_x = v; };
void foo_O_y(foo_ctx* ctx, _bool v) { ctx->_y = v; };
void foo_O_z(foo_ctx* ctx, _real v) { ctx->_z = v; };
// a little main that calls the foo.lut program
int main(){
int i = 0;
foo_ctx* ctx;
#ifdef _DEBUG
fp = fopen("debug.log", "w");
#endif
ctx = foo_new_ctx(NULL);
// lucky_set_seed(1);
printf("#inputs \"a\":int \"b\":bool \"c\":real\n");
printf("#outputs \"x\":int \"y\":bool \"z\":real\n");
for (i=1; i<10; i++){
// setting inputs
foo_I_a(ctx, i);
foo_I_b(ctx, i % 2);
foo_I_c(ctx, (_real) i);
foo_step(ctx);
printf("# step %d \n%d %d %f #outs %d %d %f\n",
i, ctx->_a, ctx->_b, ctx->_c, ctx->_x, ctx->_y, ctx->_z);
}
return 0;
}
let abs_int(x: int) = if x>=0 then x else -x
let abs_real(x: real) = if x>=0.0 then x else -x
node main(a:int; b:bool; c:real) returns ( x:int; y:bool; z:real) =
z=0.0 and x = 0
fby
loop
{
(b=>y) and abs_int(x - a) < 5 and abs_real(z - c) < 5.0
}
node env(x:int; y:bool; z:real) returns ( a:int; b:bool; c:real) =
loop true
CC = gcc -g
LD = gcc -g
EXE=
CFLAGS = \
-L `ocamlfind -query lutin` \
-I `ocamlfind -query lutin`
LIB= `ocamlfind query camlidl -l-format` \
`ocamlfind query lutin-utils -i-format` \
`ocamlfind query lutils -i-format` \
-cclib -lcamlidl -cclib -lgmp
#LIBS = -llut4c_stubs `ocamlfind query lutils -i-format` -lgmp -lm -ldl -lstdc++
LUTIN=../../../bin/lutin
ifneq (,$(findstring $(HOSTTYPE),win32))
EXE=.exe
CFLAGS = \
-L../../../lib -L/cygdrive/c/TEMP/MinGW/lib \
-I../../../include \
-Winline -Wimplicit-function-declaration
LIBS = -llut4c -llutils -lgmp -lws2_32 -lm -lstdc++
LUTIN=../../../bin/lutin$(EXE)
endif
ifeq ($(HOSTTYPE),mac)
LD = g++ -g
LIBS = -llut4c -llutils -lgmp -lm -ldl
endif
################################################################
# Calling lutin from Lustre
call_foo_loop.c:foo.c
call_foo_ext_func.c:foo.c
foo.c: foo.lut
$(LUTIN) --2c-4lustre "call_foo" -seed 42 foo.lut -m main
call_foo.ec:
../../../bin/lus2ec call_foo.lus call_foo
call_foo.c: call_foo.ec
../../../bin/ec2c$(EXE) -loop call_foo.ec
%.o : %.c
$(CC) -c $(CFLAGS) $*.c
foo$(EXE): foo.o call_foo.o call_foo_ext_func.o call_foo_loop.o
$(LD) $(CFLAGS) -o $@ $^ $(LIBS)
################################################################
clean:
rm -f run *.o *~ call_foo_ext* call_foo.c call_foo.h call_foo_loop.c call_foo_loop.h foo.h foo.c *.gp *.plot *.rif *.ec foo *.res #*
EXPDIR=`$(LUTIN) --ocaml-version`
$(EXPDIR):
[ -d $(EXPDIR) ] || (mkdir -p $(EXPDIR) ; make utest)
test.rif : clean foo$(EXE) $(EXPDIR)
echo "1 1 1 1 1 1 1 1 1 1 1" | ./foo$(EXE) > test.rif
test:test.rif
rm -f test.res && diff -B -u -i $(EXPDIR)/test.rif.exp test.rif > test.res
[ ! -s test.res ] && make clean
utest:test.rif
cp test.rif $(EXPDIR)/test.rif.exp
-- Time-stamp: <modified the 01/07/2011 (at 08:55) by Erwan Jahier>
function foo ( x:int; y:bool; z:real )
returns( a:int; b:bool; c:real );
node call_foo (dummy : int )
returns(a:int; b:bool; c:real );
let
a, b, c = foo(1 -> pre a,
true -> pre b, 10.0 -> pre c);
tel;
oc5:
module: call_foo
procedures: 1
0: foo ($1,$0,$3) ($1,$0,$3)
end:
signals: 4
0: input:dummy - single:1 bool:0
1: output:a - single:5
2: output:b - single:7
3: output:c - single:6
end:
variables: 8
0: $0
1: $1
2: $1
3: $0
4: $3
5: $1
6: $3
7: $0
end:
actions: 11
0: present: 0
1: output: 1
2: output: 2
3: output: 3
4: call:0 (2,3,4) (#1,@$1,#10.000000)
5: call:$1 (5) (2)
6: call:$3 (6) (4)
7: call:$0 (7) (3)
8: if: 7
9: call:0 (2,3,4) (5,@$1,6)
10: call:0 (2,3,4) (5,@$0,6)
end:
states: 3
startpoint: 0