source: LTS/Traces.ma @ 3375

Last change on this file since 3375 was 3374, checked in by piccolo, 6 years ago
File size: 3.1 KB
Line 
1(**************************************************************************)
2(*       ___                                                              *)
3(*      ||M||                                                             *)
4(*      ||A||       A project by Andrea Asperti                           *)
5(*      ||T||                                                             *)
6(*      ||I||       Developers:                                           *)
7(*      ||T||         The HELM team.                                      *)
8(*      ||A||         http://helm.cs.unibo.it                             *)
9(*      \   /                                                             *)
10(*       \ /        This file is distributed under the terms of the       *)
11(*        v         GNU General Public License Version 2                  *)
12(*                                                                        *)
13(**************************************************************************)
14
15include "arithmetics/nat.ma".
16include "basics/types.ma".
17include "basics/deqsets.ma".
18include "../src/ASM/Util.ma".
19
20inductive FunctionName : Type[0] ≝
21 | a_function_id : ℕ → FunctionName.
22 
23inductive CallCostLabel : Type[0] ≝
24 | a_call_label : ℕ → CallCostLabel.
25 
26inductive ReturnPostCostLabel : Type[0] ≝
27 | a_return_cost_label : ℕ → ReturnPostCostLabel.
28 
29inductive NonFunctionalLabel : Type[0] ≝
30 | a_non_functional_label : ℕ → NonFunctionalLabel.
31 
32inductive CostLabel : Type[0] ≝
33 | a_call : CallCostLabel → CostLabel
34 | a_return_post : ReturnPostCostLabel → CostLabel
35 | a_non_functional_label : NonFunctionalLabel → CostLabel.
36
37coercion a_call.
38coercion a_return_post.
39coercion a_non_functional_label.
40
41definition ret_act_label_to_cost_label :
42(ReturnPostCostLabel + NonFunctionalLabel) → CostLabel ≝
43λx.match x with [inl a ⇒ a_return_post a | inr b ⇒ a_non_functional_label b].
44
45coercion ret_act_label_to_cost_label.
46
47inductive ActionLabel : Type[0] ≝
48 | call_act : FunctionName → CallCostLabel → ActionLabel
49 | ret_act : option(ReturnPostCostLabel + NonFunctionalLabel) → ActionLabel
50 | cost_act : NonFunctionalLabel → ActionLabel
51 | tau_act : ActionLabel.
52 
53definition is_cost_label : ActionLabel → Prop ≝
54λact.match act with [ cost_act nf ⇒ True | _ ⇒ False ].
55
56record program_counter_type : Type[1] ≝
57  { pc_type : DeqSet
58  ; succ_pc : pc_type → pc_type
59  }.
60
61record abstract_status : Type[2] ≝
62 { as_status :> Type[0]
63 ; as_execute : ActionLabel → relation as_status
64 ; as_pc : program_counter_type
65 ; as_pc_of : as_status → (pc_type as_pc)
66 ; is_jump : as_status → bool
67 }.
68 
69inductive raw_trace (S : abstract_status) : option(ActionLabel) → S → S → Type[0] ≝
70  | t_base : ∀st : S.raw_trace S (None ?) st st
71  | t_ind : ∀st1,st2,st3 : S.∀m.∀l : ActionLabel.
72             as_execute S l st1 st2 → raw_trace S m st2 st3 →
73             raw_trace S (Some ? l) st1 st3.
74             
75inductive well_formed_trace (S : abstract_status) :
76   ∀st1,st2 : S.raw_trace S st1 st2 → Prop ≝
77  | t_empty : ∀st: S.well_formed_trace … (t_base S st)
78  | t_cons_uncosted :  ∀st1,st2 : .
79 
80
81
Note: See TracBrowser for help on using the repository browser.