Revision eb70bae5
Added by Christophe Garion about 6 years ago
| src/tools/stateflow/semantics/cPS_interpreter.ml | ||
|---|---|---|
| 1 |
open Basetypes
|
|
| 1 |
open Basetypes |
|
| 2 | 2 |
open Datatype |
| 3 | 3 |
(* open ActiveEnv *) |
| 4 | 4 |
open CPS_transformer |
| 5 | 5 |
(* open Simulink *) |
| 6 |
open Theta
|
|
| 6 |
open Theta |
|
| 7 | 7 |
|
| 8 | 8 |
module Interpreter (Transformer : TransformerType) = |
| 9 | 9 |
struct |
| ... | ... | |
| 165 | 165 |
match tag with |
| 166 | 166 |
| E -> fun path frontier -> Transformer.( |
| 167 | 167 |
Log.report ~level:sf_level (fun fmt -> Format.fprintf fmt "@[<v 2>S_%a[[node %a, dest %a, frontier %a]]@ " pp_tag tag pp_path p pp_path path pp_frontier frontier); |
| 168 |
((frontier = Loose) >? (eval_act (module Theta) p_def.state_actions.entry_act >> eval_act (module Theta) (open_path p))) >>
|
|
| 168 |
((frontier = Loose) >? (eval_act (module Theta) p_def.state_actions.entry_act >> eval_act (module Theta) (open_path p))) >> |
|
| 169 | 169 |
match path with |
| 170 | 170 |
| [] -> eval_C E p p_def.internal_composition |
| 171 | 171 |
| s::path_tl -> Theta.theta E (p@[s]) path_tl Loose |
| ... | ... | |
| 195 | 195 |
module type ProgType = |
| 196 | 196 |
sig |
| 197 | 197 |
val init : state_name_t |
| 198 |
val defs : src_components_t list |
|
| 198 |
val defs : prog_t src_components_t list
|
|
| 199 | 199 |
end |
| 200 | 200 |
|
| 201 | 201 |
module type EvaluationType = |
| ... | ... | |
| 204 | 204 |
val eval_prog : Transformer.t |
| 205 | 205 |
val eval_components : 'c call_t -> ('c * Transformer.t) list
|
| 206 | 206 |
end |
| 207 |
|
|
| 207 |
|
|
| 208 | 208 |
module Evaluation (Thetaify : ThetaifyType) (Prog : ProgType) : EvaluationType = |
| 209 | 209 |
struct |
| 210 | 210 |
module Denotation = Denotation (Thetaify) |
| ... | ... | |
| 216 | 216 |
let kenv = |
| 217 | 217 |
List.fold_left ( |
| 218 | 218 |
fun accu d -> match d with |
| 219 |
| State (p, defp) -> { accu with cont_node = (p, ((fun kenv -> eval_S kenv E p defp), (fun kenv -> eval_S kenv D p defp), (fun kenv -> eval_S kenv X p defp)))::accu.cont_node }
|
|
| 220 |
| Junction (j, defj) -> { accu with cont_junc = (j, (fun kenv -> eval_T kenv defj))::accu.cont_junc }
|
|
| 221 |
) {cont_node = []; cont_junc = []} Prog.defs
|
|
| 219 |
| State (p, defp) -> { accu with cont_node = (p, ((fun kenv -> eval_S kenv E p defp),
|
|
| 220 |
(fun kenv -> eval_S kenv D p defp), |
|
| 221 |
(fun kenv -> eval_S kenv X p defp)))::accu.cont_node } |
|
| 222 |
| Junction (j, defj) -> { accu with cont_junc = (j, (fun kenv -> eval_T kenv defj))::accu.cont_junc }
|
|
| 223 |
| SFFunction _ -> accu |
|
| 224 |
) {cont_node = []; cont_junc = []} Prog.defs
|
|
| 222 | 225 |
end |
| 223 | 226 |
|
| 224 | 227 |
module AppDenotation = Denotation (Kenv) |
Also available in: Unified diff
parser-json: final version of parser with new types