source: LTS/Traces.ma @ 3372

Last change on this file since 3372 was 3372, checked in by piccolo, 6 years ago

Added new implementation of labelling approach based on LTS and emmission of costlabels during transitions

File size: 2.7 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".
18
19inductive FunctionName : Type[0] ≝
20 | a_function_id : ℕ → FunctionName.
21 
22inductive CallCostLabel : Type[0] ≝
23 | a_call_label : ℕ → CallCostLabel.
24 
25inductive ReturnPostCostLabel : Type[0] ≝
26 | a_return_cost_label : ℕ → ReturnPostCostLabel.
27 
28inductive NonFunctionalLabel : Type[0] ≝
29 | a_non_functional_label : ℕ → NonFunctionalLabel.
30 
31inductive CostLabel : Type[0] ≝
32 | a_call : CallCostLabel → CostLabel
33 | a_return_post : ReturnPostCostLabel → CostLabel
34 | a_non_functional_label : NonFunctionalLabel → CostLabel.
35
36coercion a_call.
37coercion a_return_post.
38coercion a_non_functional_label.
39
40definition ret_act_label_to_cost_label :
41(ReturnPostCostLabel + NonFunctionalLabel) → CostLabel ≝
42λx.match x with [inl a ⇒ a_return_post a | inr b ⇒ a_non_functional_label b].
43
44coercion ret_act_label_to_cost_label.
45
46inductive ActionLabel : Type[0] ≝
47 | call_act : FunctionName → CallCostLabel → ActionLabel
48 | ret_act : option(ReturnPostCostLabel + NonFunctionalLabel) → ActionLabel
49 | cost_act : NonFunctionalLabel → ActionLabel
50 | tau_act : ActionLabel.
51
52record program_counter_type : Type[1] ≝
53  { pc_type : DeqSet
54  ; succ_pc : pc_type → pc_type
55  }.
56
57record abstract_status : Type[2] ≝
58 { as_status :> Type[0]
59 ; as_execute : ActionLabel → relation as_status
60 ; as_pc : program_counter_type
61 ; as_pc_of : as_status → (pc_type as_pc)
62 ; is_jump : as_status → bool
63 }.
64 
65inductive raw_trace (S : abstract_status) : S → S → Type[0] ≝
66  | t_base : ∀st : S.raw_trace S st st
67  | t_ind : ∀st1,st2,st3 : S.∀l : ActionLabel.
68             as_execute S l st1 st2 → raw_trace S st2 st3 → raw_trace S st1 st3.
69
70
Note: See TracBrowser for help on using the repository browser.