Skip to content
Projects
Groups
Snippets
Help
Loading...
Help
Support
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
T
tiamo
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
4
Issues
4
List
Boards
Labels
Milestones
Merge Requests
0
Merge Requests
0
Analytics
Repository Analytics
Value Stream Analytics
Wiki
Wiki
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Commits
Issue Boards
Open sidebar
Maximilien COLANGE
tiamo
Commits
5c1cb14e
Commit
5c1cb14e
authored
Mar 31, 2016
by
Maximilien Colange
1
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
LU bounds are now computed locally and onthefly.
It is no longer possible to compute a global M bounds.
parent
84a2fc7f
Changes
1
Hide whitespace changes
Inline
Sidebyside
Showing
1 changed file
with
209 additions
and
147 deletions
+209
147
src/uppaalta.ml
src/uppaalta.ml
+209
147
No files found.
src/uppaalta.ml
View file @
5c1cb14e
...
...
@@ 112,7 +112,9 @@ struct
}
and
location
=
{
locId
:
int
;
(* the ID of the location *)
mutable
locName
:
string
;
(* the name of the location, for printing purposes *)
locCommitted
:
bool
;
locUrgent
:
bool
;
locInvar
:
guard
;
...
...
@@ 121,6 +123,12 @@ struct
locRate
:
Costs
.
loc_rate
;
(* the cost rate of time elapsing in this location [default is None] *)
(* the cost rate of an array of location is the sum of their cost rates *)
mutable
compExpr
:
((
expression
list
)
*
(
expression
list
))
array
;
(* compExpr.(cl) contains the set of expressions against which cl is
* compared in any guard or invariant from the current location until
* it is reset. First component for L bounds, second one for U bounds.
* Local computation of LU bounds, useful for the global computation.
*)
}
and
process
=
{
procName
:
string
;
...
...
@@ 581,23 +589,9 @@ struct
in
eval_query
ta
.
query
let
lubounds
ta
state
=
DSHashtbl
.
find
ta
.
lubounds_tbl
state
(* TODO *)
let
global_mbounds
ta
=
if
(
ta
.
global_mbounds
.
(
0
)
<>
0
)
then
(
let
nclocks
=
VarContext
.
size
(
clocks
ta
)
in
ta
.
global_mbounds
.
(
0
)
<
0
;
DSHashtbl
.
iter
(
fun
_
>
fun
(
lbound
,
ubound
)
>
for
cl
=
0
to
nclocks

1
do
ta
.
global_mbounds
.
(
cl
)
<
max
ta
.
global_mbounds
.
(
cl
)
lbound
.
(
cl
);
ta
.
global_mbounds
.
(
cl
)
<
max
ta
.
global_mbounds
.
(
cl
)
ubound
.
(
cl
)
done
)
ta
.
lubounds_tbl
;
Array
.
iteri
(
fun
cl
m
>
if
(
m
<
0
)
then
printf
"clock %d (of bound %d) is never read!?
\n
"
cl
m
)
ta
.
global_mbounds
);
ta
.
global_mbounds
failwith
"not implemented"
(** print functions *)
let
print_discrete_state
chan
ta
state
=
...
...
@@ 612,140 +606,207 @@ struct
Array
.
iter
(
fun
proc
>
fprintf
chan
"%s
\n

\n
"
(
string_of_process
ta
proc
))
ta
.
procs
(********** LOADING FUNCTIONS **********)
(* propagate the clocks given in input, and return a set of clocks still
* worth to propagate
*)
let
propagate
lparent
uparent
lson
uson
updates
clocks
=
let
res
=
ref
ClockSet
.
empty
in
(* for every element of clocks, check whether to propagate *)
ClockSet
.
iter
(
fun
cl
>
(* a clock does not propagate past an update *)
if
(
List
.
for_all
(
fun
(
i
,_
)
>
i
<>
cl
)
updates
)
then
begin
(* a clock is worth propagating later on if it propagates here *)
if
(
lparent
.
(
cl
)
<
lson
.
(
cl
))
then
(
lparent
.
(
cl
)
<
lson
.
(
cl
);
res
:=
ClockSet
.
add
cl
!
res
);
if
(
uparent
.
(
cl
)
<
uson
.
(
cl
))
then
(
uparent
.
(
cl
)
<
uson
.
(
cl
);
res
:=
ClockSet
.
add
cl
!
res
)
end
)
clocks
;
!
res
exception
Early_stop
(** To compute LU (and M) bounds, we first explore the whole discrete
* state space.
* At each discrete state s, each clock c is given the largest constant
* against which it is compared in s.
* Then, larger bounds propagate backwards, but not CROSS resets.
* The best way to do this (with the retropropagation) is a DFS of the
* discrete state space
*)
(* TODO by adapting the walk order, the M bounds could be computed on the fly,
* while the real state space is being discovered
(** given a set of expressions, simplify it to retain only its maximal
* constant and all nonconstant *)
(* TODO check that the input does not contain ConstVariable or constant ConstArray *)
let
simplify_max
exprs
=
let
new_max
=
function

None
>
(
function

Constant
k
>
Some
k

_
>
None
)

Some
m
as
e
>
(
function

Constant
k
when
k
>
m
>
Some
k

_
>
e
)
in
match
List
.
fold_left
new_max
None
exprs
with

None
>
exprs

Some
k
>
List
.
filter
(
function

Constant
l
when
l
<
k
>
false

_
>
true
)
exprs
(* given a process, a location l and a clock c, compute the set of expressions
* against which c is compared from l until it is reset.
* Formally, the result S is the smallest set of expressions such that:
* if x is compared to e in the invariant of l, then e \in S
* for any transition t : l>l'
* if x is compared to e in the guard of t, then e \in S
* if x is not reset in t, then comp_expressions p l' c \subset S
* returns a pair (L,U)
*)
let
comp_expressions
ta
p
l
c
=
ta
.
procs
.
(
p
)
.
procLocations
.
(
l
)
.
compExpr
.
(
c
)
(* computes the LU bounds in a given state *)
(* this should be used from another function that caches the results *)
(* TODO some clocks already have their constant known, cache them *)
let
_lubounds
ta
state
=
let
n
=
nb_clocks
ta
in
let
lb
,
ub
=
Array
.
make
n
0
,
Array
.
make
n
0
in
for
cl
=
0
to
n

1
do
let
lexpr
,
uexpr
=
Array
.
fold_left
(
fun
(
lacc
,
uacc
)
loc
>
let
ltmp
,
utmp
=
loc
.
compExpr
.
(
cl
)
in
(
lacc
@
ltmp
,
uacc
@
utmp
))
([]
,
[]
)
state
.
stateLocs
in
(* instantiate found expressions, and retain only the maximal constant *)
let
lcst
,
ucst
=
simplify_max
(
List
.
map
(
fun
e
>
eval_exp
ta
state
.
stateVars
e
)
lexpr
)
,
simplify_max
(
List
.
map
(
fun
e
>
eval_exp
ta
state
.
stateVars
e
)
uexpr
)
in
begin
match
lcst
with

(
Constant
k
)
::_
>
lb
.
(
cl
)
<
max
lb
.
(
cl
)
k

_
>
(* TODO can it happen? *)
()
end
;
begin
match
ucst
with

(
Constant
k
)
::_
>
ub
.
(
cl
)
<
max
ub
.
(
cl
)
k

_
>
(* TODO can it happen? *)
()
end
;
done
;
lb
,
ub
let
lubounds
ta
state
=
try
DSHashtbl
.
find
ta
.
lubounds_tbl
state
with

Not_found
>
let
res
=
_lubounds
ta
state
in
DSHashtbl
.
add
ta
.
lubounds_tbl
state
res
;
res
(* tells whether a given clock is set by a given update *)
(* the difficult part is when the lhs of the update is an array cell *)
let
is_reset
:
clock_t
>
update
>
bool
=
fun
cl
>
function

ClockRef
c
,
_
when
c
=
cl
>
true

ClockArrayRef
(
a
,_
)
,
_
>
(* TODO true if cl is a cell of the array a, false otherwise *)
(* TODO further refine: if all indices expressions are constant, we
* can do an exact equality check *)
failwith
"cannot compute bounds for arrays of clocks"

_
>
false
(* return the set of clock the argument can refer to *)
let
clocks_of
ta
=
function

Clock
c
>
[
c
]

ClockArray
(
a
,_
)
>
(*TODO*)
failwith
"cannot compute bounds for arrays of clocks"

_
>
[]
(* compute all the local LU bounds *)
let
build_lu
ta
=
let
nclocks
=
VarContext
.
size
ta
.
clocks
in
let
trace
=
Stack
.
create
()
in
(* trace is a stack of discrete_state * (transition list) *)
(* to get a list of transitions from a discrete state, use _transitions_from *)
let
init
=
initial_state
ta
in
let
init_edges
=
_transitions_from
ta
init
in
Stack
.
push
(
init
,
init_edges
)
trace
;
let
ltmp
,
utmp
=
Array
.
make
nclocks
min_int
,
Array
.
make
nclocks
min_int
in
DSHashtbl
.
add
ta
.
lubounds_tbl
init
(
ltmp
,
utmp
);
while
(
not
(
Stack
.
is_empty
trace
))
do
let
(
current
,
edges
)
=
Stack
.
top
trace
in
match
edges
with

[]
>
begin
(* pop the stack *)
let
_
=
Stack
.
pop
trace
in
(* we are done with this state, retropropagation *)
let
son
=
ref
current
in
let
clocks
=
ref
ClockSet
.
empty
in
for
cl
=
1
to
nclocks

1
do
clocks
:=
ClockSet
.
add
cl
!
clocks
done
;
(* Do the bound retropropagation *)
begin
try
Stack
.
iter
(
fun
(
parent
,
edge
::
_
)
>
if
(
ClockSet
.
is_empty
!
clocks
)
then
raise
Early_stop
;
let
lson
,
uson
=
DSHashtbl
.
find
ta
.
lubounds_tbl
!
son
in
let
lparent
,
uparent
=
DSHashtbl
.
find
ta
.
lubounds_tbl
parent
in
let
(
_
,_,
updates
,_
)
=
transition_fields
ta
edge
in
clocks
:=
propagate
lparent
uparent
lson
uson
updates
!
clocks
;
son
:=
parent
)
trace
;
with

Early_stop
>
()
end
;
(* get the parent state, its first edge is the one between parent and current *)
if
(
not
(
Stack
.
is_empty
trace
))
then
(
let
(
parent
,
_
::
l
)
=
Stack
.
pop
trace
in
(* repush the parent and its remaining edges *)
Stack
.
push
(
parent
,
l
)
trace
;
)
end

edge
::
rest
>
begin
let
(
_
,
guard
,
updates
,
succ
)
=
transition_fields
ta
edge
in
let
(
current_lower
,
current_upper
)
=
DSHashtbl
.
find
ta
.
lubounds_tbl
current
in
(* evaluate accesses to clock arrays, if any *)
(* TODO refactor: the guard should already be evaluated by _transition_fields *)
let
evalClock
=
fun
(
ClockArray
(
i
,
ilist
))
>
let
indices
=
List
.
map
(
fun
e
>
eval_disc_exp
ta
current
.
stateVars
e
)
ilist
in
let
cid
=
VarContext
.
index_of_cell
ta
.
clocks
i
indices
in
Clock
(
cid
)
in
let
guard_eval
=
List
.
map
(
function

GuardLeq
(
ClockArray
(
_
,_
)
as
ca
,
rhs
)
>
GuardLeq
(
evalClock
ca
,
rhs
)

GuardLess
(
ClockArray
(
_
,_
)
as
ca
,
rhs
)
>
GuardLess
(
evalClock
ca
,
rhs
)

GuardEqual
(
ClockArray
(
_
,_
)
as
ca
,
rhs
)
>
GuardEqual
(
evalClock
ca
,
rhs
)

GuardGeq
(
ClockArray
(
_
,_
)
as
ca
,
rhs
)
>
GuardGeq
(
evalClock
ca
,
rhs
)

GuardGreater
(
ClockArray
(
_
,_
)
as
ca
,
rhs
)
>
GuardGeq
(
evalClock
ca
,
rhs
)

_
as
x
>
x
)
guard
in
(* update the bounds of current thanks to current transition *)
List
.
iter
(
function

GuardLeq
(
Clock
(
cl
)
,
e
)

GuardLess
(
Clock
(
cl
)
,
e
)
>
let
r
=
eval_disc_exp
ta
current
.
stateVars
e
in
current_upper
.
(
cl
)
<
max
current_upper
.
(
cl
)
r

GuardEqual
(
Clock
(
cl
)
,
e
)
>
let
r
=
eval_disc_exp
ta
current
.
stateVars
e
in
current_upper
.
(
cl
)
<
max
current_upper
.
(
cl
)
r
;
current_lower
.
(
cl
)
<
max
current_lower
.
(
cl
)
r

GuardGeq
(
Clock
(
cl
)
,
e
)

GuardGreater
(
Clock
(
cl
)
,
e
)
>
let
r
=
eval_disc_exp
ta
current
.
stateVars
e
in
current_lower
.
(
cl
)
<
max
current_lower
.
(
cl
)
r

_
>
failwith
"cannot compute LU bounds, guard not in normal form"
)
guard_eval
;
(* now take care of the succ *)
if
(
DSHashtbl
.
mem
ta
.
lubounds_tbl
succ
)
then
(* if already discovered, push it on the stack with an empty list of
* edges in order to have the correct retropropagation *)
begin
Stack
.
push
(
succ
,
[]
)
trace
end
else
(* if new, add it to the hashtable and push it on the stack *)
begin
let
ltmp
,
utmp
=
Array
.
make
nclocks
min_int
,
Array
.
make
nclocks
min_int
in
DSHashtbl
.
add
ta
.
lubounds_tbl
succ
(
ltmp
,
utmp
);
let
succ_edges
=
_transitions_from
ta
succ
in
Stack
.
push
(
succ
,
succ_edges
)
trace
end
end
done
;
DSHashtbl
.
iter
(
fun
_
>
fun
(
lbound
,
ubound
)
>
for
cl
=
0
to
nclocks

1
do
if
(
lbound
.
(
cl
)
<
0
)
then
lbound
.
(
cl
)
<
0
;
if
(
ubound
.
(
cl
)
<
0
)
then
ubound
.
(
cl
)
<
0
done
)
ta
.
lubounds_tbl
(* for each process *)
for
p
=
0
to
(
Array
.
length
ta
.
procs
)

1
do
let
proc
=
ta
.
procs
.
(
p
)
in
(* initialization: for each location, add the expression of its invariant
* and of guards of outgoing transitions
*)
for
l
=
0
to
(
Array
.
length
proc
.
procLocations
)

1
do
let
loc
=
proc
.
procLocations
.
(
l
)
in
loc
.
compExpr
<
Array
.
make
nclocks
([]
,
[]
);
let
ag_handle
=
function

GuardLeq
(
lhs
,
e
)

GuardLess
(
lhs
,
e
)
>
List
.
iter
(
fun
cl
>
let
ltmp
,
utmp
=
loc
.
compExpr
.
(
cl
)
in
if
not
(
List
.
mem
e
utmp
)
then
loc
.
compExpr
.
(
cl
)
<
ltmp
,
e
::
utmp
)
(
clocks_of
ta
lhs
)

GuardGeq
(
lhs
,
e
)

GuardGreater
(
lhs
,
e
)
>
List
.
iter
(
fun
cl
>
let
ltmp
,
utmp
=
loc
.
compExpr
.
(
cl
)
in
if
not
(
List
.
mem
e
ltmp
)
then
loc
.
compExpr
.
(
cl
)
<
e
::
ltmp
,
utmp
)
(
clocks_of
ta
lhs
)

GuardEqual
(
lhs
,
e
)
>
List
.
iter
(
fun
cl
>
let
ltmp
,
utmp
=
loc
.
compExpr
.
(
cl
)
in
let
lnew
=
if
not
(
List
.
mem
e
ltmp
)
then
e
::
ltmp
else
ltmp
in
let
unew
=
if
not
(
List
.
mem
e
utmp
)
then
e
::
utmp
else
utmp
in
loc
.
compExpr
.
(
cl
)
<
lnew
,
unew
)
(
clocks_of
ta
lhs
)

_
>
failwith
"cannot compute LU bounds, guard is not in normal form"
in
(* add invariant contribution *)
List
.
iter
ag_handle
loc
.
locInvar
;
(* for each transition, add guard contribution *)
List
.
iter
(
fun
edge
>
List
.
iter
ag_handle
edge
.
edgeGuard
)
loc
.
locEdges
done
;
(* fixpoint computation
* for each location l, for each transition t from l to l',
* for each clock c,
* if c is not reset by t, add the expressions for c from l' in l
* if the set for l changes in the operation, remember to loop once more
*)
let
stable
=
ref
false
in
while
not
!
stable
do
stable
:=
true
;
(* for each location *)
for
l
=
0
to
(
Array
.
length
proc
.
procLocations
)

1
do
let
loc
=
proc
.
procLocations
.
(
l
)
in
(* iterate over the transitions *)
List
.
iter
(
fun
edge
>
(* for each clock *)
for
cl
=
0
to
nclocks

1
do
(* if it is not reset *)
if
List
.
for_all
(
fun
u
>
not
(
is_reset
cl
u
))
edge
.
edgeUpdates
then
begin
let
lcurrent
,
ucurrent
=
loc
.
compExpr
.
(
cl
)
in
(* update lower bounds *)
let
lnew
=
List
.
fold_left
(
fun
acc
e
>
if
not
(
List
.
mem
e
acc
)
then
(
stable
:=
false
;
e
::
acc
)
else
(
acc
)
)
lcurrent
(
fst
proc
.
procLocations
.
(
edge
.
edgeTarget
)
.
compExpr
.
(
cl
))
in
(* update upper bounds *)
let
unew
=
List
.
fold_left
(
fun
acc
e
>
if
not
(
List
.
mem
e
acc
)
then
(
stable
:=
false
;
e
::
acc
)
else
(
acc
)
)
ucurrent
(
snd
proc
.
procLocations
.
(
edge
.
edgeTarget
)
.
compExpr
.
(
cl
))
in
(* do the actual update *)
loc
.
compExpr
.
(
cl
)
<
lnew
,
unew
end
done
)
loc
.
locEdges
done
done
done
(** Constructs a timed_automaton from the C data structure produced by the
* library utap.
...
...
@@ 1020,6 +1081,7 @@ struct
locEdges
=
edges
;
locProc
=
procId
;
locRate
=
costRate
;
compExpr
=
Array
.
make
0
([]
,
[]
);
(* actually built during LU bounds computation *)
}
in
Callback
.
register
"cb_build_location"
build_location
;
...
...
Maximilien COLANGE
@colange
mentioned in commit
87cad902
·
Apr 04, 2016
mentioned in commit
87cad902
mentioned in commit 87cad902bf63d4f5b130d7d0633b7f870c21fe71
Toggle commit list
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment