Changeset 3035 for src/semantics.ma
- Timestamp:
- Mar 29, 2013, 3:21:49 PM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/semantics.ma
r3014 r3035 34 34 λ_.mk_preclassified_system_pass … (joint_preclassified_system LTL_semantics) … 35 35 | lin_pass ⇒ 36 λ_.mk_preclassified_system_pass lin_pass (joint_preclassified_system LIN_semantics) ?36 λ_.mk_preclassified_system_pass lin_pass (joint_preclassified_system LIN_semantics) … 37 37 | assembly_pass ⇒ 38 38 λprog. let 〈code,sigma,policy〉 ≝ prog in 39 39 mk_preclassified_system_pass … (ASM_preclassified_system code sigma policy) … 40 40 | object_code_pass ⇒ 41 λprog. mk_preclassified_system_pass ?(OC_preclassified_system prog) …41 λprog. mk_preclassified_system_pass … (OC_preclassified_system prog) … 42 42 ]. 43 43 % … … 49 49 ≝ 50 50 λpass,prog,n,print_pass,print_event,print_error,print_exit. 51 let pcs ≝ preclassified_system_of_pass pass prog in 51 let res ≝ 52 let pcs ≝ preclassified_system_of_pass pass prog in 52 53 let prog ≝ prog⌈syntax_of_pass pass ↦ ?⌉ in 53 54 let g ≝ make_global … pcs prog in 54 match make_initial_state … pcs prog with55 [ Error msg ⇒ print_error msg56 | OK s0 ⇒57 let i ≝ print_pass pass in58 let 〈trace,res〉 ≝ observe_all_in_measurable n (pcs_to_cs pcs …) print_event [ ] s0 in59 55 ! s0 ← make_initial_state … pcs prog ; 56 let i ≝ print_pass pass in 57 let 〈trace,res〉 ≝ observe_all_in_measurable n (pcs_to_cs pcs …) print_event [ ] s0 in 58 res 59 in 60 match res with 60 61 [ OK n ⇒ print_exit n 61 | Error msg ⇒ print_error msg ]]. 62 | Error msg ⇒ print_error msg ] 63 . 62 64 @pcs_ok 63 65 qed.
Note: See TracChangeset
for help on using the changeset viewer.