Commit d8f56437 authored by mcolange's avatar mcolange

Directly provide fields of transitions, instead of going through the 'transition_fields' method.

parent c996f56b
......@@ -289,8 +289,7 @@ struct
DSHashtbl.find transitions_cache loc
with
| Not_found ->
let tlist = List.map (fun t ->
TA.transition_fields ta t) (TA.transitions_from ta loc)
let tlist = TA.transitions_from ta loc
in
DSHashtbl.add transitions_cache loc tlist;
tlist
......@@ -370,8 +369,7 @@ struct
with
| Not_found ->
let tlist = List.rev_append
(List.map (fun t -> TA.transition_fields ta t)
(TA.transitions_from ta loc))
(TA.transitions_from ta loc)
(bounding_transitions loc ta)
in
DSHashtbl.add transitions_cache loc tlist;
......
......@@ -18,7 +18,8 @@ sig
val initial_discrete_state : timed_automaton -> discrete_state
(* does it belong here? If so, so does type for extended_state... *)
val initial_extended_state : timed_automaton -> discrete_state * MDbm.Dbm.t
val transitions_from : timed_automaton -> discrete_state -> transition list
val transitions_from : timed_automaton -> discrete_state ->
(discrete_state * UDbm.Dbm.t * ((clock_t * int) list) * discrete_state) list
val transition_fields : timed_automaton -> transition ->
(discrete_state * UDbm.Dbm.t * ((clock_t * int) list) * discrete_state)
val guard_of_transition : timed_automaton -> transition -> UDbm.Dbm.t
......@@ -511,7 +512,7 @@ struct
Dbm.set_zero z;
(ta.init, z)
let transitions_from ta state =
let _transitions_from ta state =
let committed = is_committed state in
let transq = Queue.create () in
(* Queue of synchronizing edges *)
......@@ -580,6 +581,9 @@ struct
let g = guard_of_transition ta tr in
(state, g, e1.edgeReset @ e2.edgeReset, state')
let transitions_from ta state =
List.map (fun tr -> transition_fields ta tr) (_transitions_from ta state)
let is_urgent_or_committed ta state =
let rec aux ar n =
if (ar.(n).locCommitted || ar.(n).locUrgent) then true
......
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