Commit cbed4829 authored by erwan's avatar erwan

git add or git ignore untracked files.

parent 0f939d61
......@@ -36,6 +36,7 @@ src/lexer.mli
xx
xxx
bin
#*
*.output
*.lnk
camlidl-*
......@@ -204,6 +205,7 @@ examples/lutin/catherine
examples/lutin/simplice
examples/lutin/chaouki
*.annot
*.seed
*.out
VALORISATION
examples/*/*/*.*.*/
......@@ -245,3 +247,26 @@ sh/
Makefile.common.source
TODO
user-rules
GBDDML
RUN_ME
README-*
LIMITATIONS.portage_scade
TODO.SCADEGUI
doc/lutin-tuto/mes_styles.css
doc/lutin-tuto/my-rdbg-tuning.ml
doc/lutin-tuto/theme-bigblow.setup
doc/lutin-tuto/worg-classic.css
doc/lutin-tuto/worg-r1.css
doc/lutin-tuto/worg-zenburn.css
examples/lutin/xlurette/call-luciole/my-rdbg-tuning.ml
install/
lnsw
lnsw-clean
lutin.native
polka/C/
polka/caml/
source/
src/
#######################################################################################
# Workflow:
# C=git commit ; A=git amend ; U=update_version ; OP=opam pack
# to make sure the sha and the version are good, one should never
# do U and then A.
# to avoid such problems, legal trace are defined by this automata:
# C=git commit ; A=git amend ; U=update_version ; P=opam pack
# - to make sure the sha and the version are good, one should never
# do U and then A.
# - to make sure gtit is not confused, one should never do A and the P
#
# thereforeto avoid such problems, legal trace are defined by this automata:
# 0 -C-> 1
# 1 -OP-> 1
# 1 -A-> 1
# 1 -P-> 2
# 2 -U-> 0
# 1 -U-> 0
# to implement such a workflow, C puts a lock (state 1) and U removes it (state 0)
# To enforce its use, one has to use git via "make uv/ci/cia/amend"
###############################
# a few git shortcuts
......@@ -34,10 +37,13 @@ ci:
echo "*** I won't commit!\n*** until you 'make update_version'!" \
|| (git commit -F log && touch committed)
push:
git push && make uv
amend:
test -f committed && git commit -a -F log --amend
dif:
git --no-pager diff --color-words
diff:dodiff
......
This diff is collapsed.
let n = 3
node ok_since_n_instants(b:bool) returns (res:bool) =
exist cpt: int = n in
loop {
cpt = (if b then (pre cpt-1) else n) and
res = (b and (cpt <= 0))
}
node ok_since_n_instants(b:bool;n:int)returns(res:bool)=
exist cpt: int in
cpt = n and res = (b and (cpt <= 0))
fby
loop {
cpt = (if b then (pre cpt-1) else n) and
res = (b and (cpt <= 0))
}
(* File generated from lutinUtils.idl *)
external gauss_continue : int -> int -> int -> int
= "camlidl_lutinUtils_gauss_continue"
external gauss_stop : int -> int -> int -> int
= "camlidl_lutinUtils_gauss_stop"
external interval_continue : int -> int -> int -> int
= "camlidl_lutinUtils_interval_continue"
external interval_stop : int -> int -> int -> int
= "camlidl_lutinUtils_interval_stop"
(* File generated from lutinUtils.idl *)
external gauss_continue : int -> int -> int -> int
= "camlidl_lutinUtils_gauss_continue"
external gauss_stop : int -> int -> int -> int
= "camlidl_lutinUtils_gauss_stop"
external interval_continue : int -> int -> int -> int
= "camlidl_lutinUtils_interval_continue"
external interval_stop : int -> int -> int -> int
= "camlidl_lutinUtils_interval_stop"
let str="2.32"
let sha="c09cc68"
let sha="0f939d6"
-- The examples provided is the [SIES'13] "Engineering Functional
-- Requirements of Reactive Systems using Synchronous Languages"
node gen_x_v1() returns (x:real) = loop 0.0<x and x<42.0
node gen_x_v2() returns (x:real) =
loop { 0.0<x and x<42.0 fby loop [20] x = pre x }
node gen_x_v3() returns (target:real; x:real=0.0) =
run target := gen_x_v2() in
loop { x = (pre x + target) / 2.0 }
let inertia=0.6
node gen_x_v4() returns (target:real; x:real=0.0) =
run target := gen_x_v2() in
exist px,ppx : real = 0.0 in
loop {
px = pre x and ppx = pre px and
x = (px+target) / 2.0+inertia*(px-ppx)
}
let Between(x, min, max : real) : bool = ((min < x) and (x < max))
node between (min, max : real) returns (x:real) =
loop ((min < x) and (x < max))
-- saw shark curves
node up(init, delta:real) returns( x : real) =
x = init fby loop { Between(x, pre x, pre x + delta) }
node down(init, delta:real) returns( x : real) =
x = init fby loop { Between(x, pre x - delta, pre x) }
node up_and_down(min, max, delta : real) returns (x : real) =
Between(x, min, max)
fby
loop {
| run x := up(pre x, delta) in loop { x < max }
| run x := down(pre x, delta) in loop { x > min }
}
-- Similar to up and down, except that the min, max, and delta are
-- chosen randomly at each round
node up_and_down2(min, max, delta : real) returns (x : real) =
Between(x, min, max)
fby
loop
exist lmin, lmax,ldelta : real in
run lmin := between(min, pre x) in
run lmax := between(pre x, max) in
run ldelta := between(0., delta) in
{
| run x := up(pre x, ldelta) in loop { x < lmax }
| run x := down(pre x, ldelta) in loop { x > lmin }
}
node exemple_of_use_of_up_and_down () returns (x,y : real) =
run x:= up_and_down (0.0, 100.0, 5.0) in
run y:= up_and_down2(0.0, 100.0, 5.0)
-- Time-stamp: <modified the 08/07/2016 (at 10:45) by Erwan Jahier>
-- Mimick the content of the Stimulus Temporal library
let OnceNow(condition:bool): trace = condition
let Repeat(BODY:trace) : trace = loop BODY
let Always(condition:bool) : trace = loop condition
let DoAfterwards(DO,AFTER: trace) : trace = DO fby AFTER
let AlwaysDuring(duration:int; condition:bool) : trace = loop [duration] condition
let AsLongAs(event:bool; BODY:trace) : trace = assert event in BODY
let From(event:bool; BODY:trace) : trace = loop not event fby BODY
let Until(event:bool; BODY:trace) : trace = assert not event in BODY
let OnceWithin(delay:int; condition:bool) : trace =
loop [0,delay] not condition fby condition
let AlwaysUntil(condition,event:bool) : trace =
assert condition in loop not event fby event
let OnceBefore(condition,event:bool) : trace =
loop { not (event and condition)} fby
event and condition
let when(condition:bool; BODY:trace) : trace =
loop {
| assert condition in BODY
| not condition
}
let IfThenElse(condition:bool;THEN,ELSE: trace) : trace = {
|> { condition &> THEN }
|> ELSE
}
-- Tests
let integers(init: int; cpt: int ref):trace =
cpt = init fby loop cpt = 1 + pre cpt
node test_when(condition:bool) returns (res:int) =
when(condition, integers(0,res))
node test_AsLongAs(condition:bool) returns (res:int) =
AsLongAs(condition, integers(0,res))
node test_From(condition:bool) returns (res:int) =
From(condition, integers(0,res))
node test_Until(condition:bool) returns (res:int) =
Until(condition, integers(0,res))
node test_IfThenElse(condition:bool) returns (res:int) =
IfThenElse(condition, integers(0,res), integers(-100,res))
node test_DoAfterwards() returns (res:int) =
DoAfterwards( loop [2,5] res = 0, loop [2] res=1)
node test_Repeat() returns (res:int) =
Repeat (res=0 fby res=1 fby res=2)
node test_OnceBefore(event : bool) returns( condition : bool) =
OnceBefore(condition,event)
node main(event:bool) returns (res:int) =
trap stop in
{ &> loop event fby raise stop
&> integers(0,res)
} fby
raise stop
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment