|
Last change
on this file since 3096 was
2968,
checked in by sacerdot, 8 years ago
|
|
The initial status memory was not really initialized. Now it is.
|
|
File size:
1.0 KB
|
| Line | |
|---|
| 1 | include "joint/Traces.ma". |
|---|
| 2 | include "common/Measurable.ma". |
|---|
| 3 | |
|---|
| 4 | definition joint_exec: sem_params → trans_system io_out io_in ≝ |
|---|
| 5 | λG.mk_trans_system ?? (evaluation_params G) (λ_. state_pc G) |
|---|
| 6 | (λenv.joint_final … env) |
|---|
| 7 | (λenv.λst.! st' ← eval_state … env st ; |
|---|
| 8 | let charge ≝ match joint_label_of_pc … env (pc … st) with |
|---|
| 9 | [ Some c ⇒ Echarge c | None ⇒ E0 ] in |
|---|
| 10 | return 〈charge, st'〉). |
|---|
| 11 | |
|---|
| 12 | definition joint_fullexec : |
|---|
| 13 | sem_params → fullexec io_out io_in ≝ |
|---|
| 14 | λG.mk_fullexec ?? (joint_program G × (ident → option ℕ)) |
|---|
| 15 | (joint_exec G) |
|---|
| 16 | (λpr.joint_make_global (mk_prog_params G (\fst pr) (\snd pr))) |
|---|
| 17 | (λp_stacks. |
|---|
| 18 | make_initial_state (mk_prog_params G (\fst p_stacks) (\snd p_stacks))). |
|---|
| 19 | |
|---|
| 20 | definition joint_preclassified_system : sem_params → |
|---|
| 21 | preclassified_system ≝ |
|---|
| 22 | λG.mk_preclassified_system (joint_fullexec G) |
|---|
| 23 | (λenv.λst.¬is_none … (joint_label_of_pc … env (pc … st))) |
|---|
| 24 | (λenv.joint_classify … env) |
|---|
| 25 | (λenv.λs.λ_.joint_call_ident … env s). |
|---|
Note: See
TracBrowser
for help on using the repository browser.
