Changeset 1233 for src/LTL


Ignore:
Timestamp:
Sep 21, 2011, 11:57:20 AM (8 years ago)
Author:
sacerdot
Message:

1) Ported to Brian's new dependent type for fullexec
2) Universe level raised for fullexec and related stuff to accomodate the

joint semantics

3) Improved joint syntax and semantics
4) Code for LTLToLin simplified

Location:
src/LTL
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/LTL/LTL.ma

    r1222 r1233  
    33
    44definition ltl_params: params ≝
    5  mk_params
    6    unit unit unit unit registers_move Register
    7      unit unit unit unit.
     5 mk_params (mk_params_ unit unit unit unit registers_move Register False unit unit unit) label.
    86
    9 definition ltl_statement ≝ λglobals: list ident. joint_statement ltl_params globals.
     7definition ltl_statement ≝ joint_statement ltl_params.
    108
    11 definition ltl_sem_params_: ∀globals. sem_params_ ltl_params globals ≝
     9(*definition ltl_sem_params_: ∀globals. sem_params_ ltl_params globals ≝
    1210 λglobals.
    13   mk_sem_params_ ltl_params globals (graph (ltl_statement globals)) (lookup …).
     11  mk_sem_params_ ltl_params globals (graph (ltl_statement globals)) (lookup …).*)
    1412
    15 definition ltl_program ≝ λglobals. joint_program globals … (ltl_sem_params_ globals).
    16 (*
    17  
    18 record ltl_internal_function (globals: list ident): Type[0] ≝
    19 {
    20   ltl_if_luniverse: universe LabelTag;
    21   ltl_if_runiverse: universe RegisterTag;
    22   ltl_if_stacksize: nat;
    23   ltl_if_graph: ltl_statement_graph globals;
    24   ltl_if_entry: Σl: label. lookup ? ? ltl_if_graph l ≠ None ?;
    25   ltl_if_exit: Σl: label. lookup ? ? ltl_if_graph l ≠ None ?
    26 }.
    27 
    28 inductive ltl_function_definition (globals: list ident): Type[0] ≝
    29   | ltl_fu_internal_function: ltl_internal_function globals → ltl_function_definition globals
    30   | ltl_fu_external_function: external_function → ltl_function_definition globals.
    31  
    32 record ltl_program (globals: list (ident × nat)): Type[0] ≝
    33 {
    34   ltl_pr_funcs: list (ident × (ltl_function_definition (map ? ? \fst globals)));
    35   ltl_pr_main: option ident
    36 }.
    37 *)
     13definition ltl_program ≝ joint_program ltl_params.
  • src/LTL/LTLToLIN.ma

    r1224 r1233  
    33include "utilities/BitVectorTrieSet.ma".
    44
    5 axiom LTLTag: String.
    6 
    7 definition translate_statement: ∀globals. ltl_statement globals → pre_lin_statement globals ≝
     5definition translate_statement: ∀globals. ltl_statement globals → lin_statement globals ≝
    86  λglobals: list ident.
    97  λs: ltl_statement globals.
    108  match s with
    11   [ joint_st_return ⇒ joint_st_return lin_params globals
    12   | joint_st_sequential instr lbl ⇒ joint_st_sequential lin_params globals instr lbl
    13   | joint_st_goto l ⇒ joint_st_goto lin_params globals l
    14   | joint_st_extension ext ⇒ joint_st_extension lin_params globals ext
     9  [ joint_st_return ⇒ joint_st_return
     10  | joint_st_sequential instr lbl ⇒ joint_st_sequential … instr it
     11  | joint_st_goto l ⇒ joint_st_goto l
     12  | joint_st_extension ext ⇒ joint_st_extension lin_params ext
    1513  ].
    16    
    17 definition require: label → BitVectorTrieSet 16 → BitVectorTrieSet 16 ≝
    18   λl: label.
    19   λg: BitVectorTrieSet 16.
    20     set_insert ? (word_of_identifier ? l) g.
    21    
    22 definition mark: label → BitVectorTrieSet 16 → BitVectorTrieSet 16 ≝
    23   λl: label.
    24   λg: BitVectorTrieSet 16.
    25     set_insert ? (word_of_identifier ? l) g.
    26    
    27 definition marked: label → BitVectorTrieSet 16 → bool ≝
    28   λl: label.
    29   λg: BitVectorTrieSet 16.
    30     set_member ? (word_of_identifier ? l) g.
    31    
    32 definition graph_lookup ≝
    33   λglobals: list ident.
    34   λl: label.
    35   λgr: graph (ltl_statement globals).
    36     lookup LabelTag ? gr (an_identifier LabelTag (word_of_identifier ? l)).
    37    
    38 definition fetch: ∀globals: list ident. label → graph (ltl_statement globals) → option (ltl_statement globals) ≝
    39   λglobals,l,g.graph_lookup globals l g.
    4014
    41 definition foo ≝
    42   λl2, visited, required, globals, generated, g, n.
    43   λvisit:
    44   ∀globals: list ident.
    45   ∀g: graph (ltl_statement globals).
    46   ∀required: BitVectorTrieSet 16.
    47   ∀visited: BitVectorTrieSet 16.
    48   ∀generated: list (pre_lin_statement globals).
    49   ∀l: label.
    50   ∀n: nat.
    51     BitVectorTrieSet 16 × (list (pre_lin_statement globals)).
    52   if marked l2 visited then
    53     〈require l2 required, (joint_st_goto … globals l2) :: generated〉
    54   else
    55    visit globals g required visited generated l2 n.
    56 
    57 (* XXX: look at this.  way too complicated to understand whether it is correct,
    58    in my opinion.
    59 *)
     15(* Invariant: l has not been visited yet the very first time the
     16   function is called and in the true branch of a conditional call.
     17   This avoid useless gotos.
     18   
     19   Note: the OCaml code contains some useful explanatory comments. *)
    6020let rec visit
    6121  (globals: list ident) (g: graph (ltl_statement globals))
    6222  (required: BitVectorTrieSet 16) (visited: BitVectorTrieSet 16)
    63   (generated: list (pre_lin_statement globals)) (l: label) (n: nat)
    64     on n: BitVectorTrieSet 16 × (list (pre_lin_statement globals)) ≝
     23  (generated: list (lin_statement globals)) (l: label) (n: nat)
     24    on n: BitVectorTrieSet 16 × (list (lin_statement globals)) ≝
    6525  match n with
    66   [ O ⇒ 〈required, generated〉
     26  [ O ⇒ ⊥ (* CSC: Case to be made impossible; use dummy value? *)
    6727  | S n' ⇒
    68     let visited' ≝ mark l visited in
    69     match fetch globals l g with
    70     [ None ⇒ 〈required, generated〉 (* dpm: correct? *)
    71     | Some statement ⇒
    72       let translated_statement ≝ translate_statement globals statement in
    73       let generated'' ≝ translated_statement :: generated in
    74       match statement with
    75       [ joint_st_sequential instr l2 ⇒
    76         match instr with
    77         [ joint_instr_cond acc_a_reg l1 ⇒
    78               let required' ≝
    79                 if marked l2 visited' then
    80                   require l2 required
    81                 else
    82                   required in
    83               let 〈required', generated''〉 ≝
    84                foo l2 visited' required' globals generated'' g n' visit (*
    85                 if marked l2 visited' then
    86                   〈required', (Joint_St_Goto ? globals l2) :: generated''〉
    87                 else
    88                   visit globals g required' visited' generated'' l2 n'*) in
    89               let required'' ≝ require l1 required' in
    90                 if ¬(marked l1 visited') then
    91                   visit globals g required'' visited' generated'' l1 n'
    92                 else
    93                   〈required', generated''〉
    94           | _ ⇒
    95             let required' ≝
    96               if marked l2 visited' then
    97                 require l2 required
    98               else
    99                 required in
    100             if marked l2 visited' then
    101               〈required', joint_st_goto … globals l2 :: generated''〉
    102             else
    103               visit globals g required' visited' generated'' l2 n'
    104           ]
    105     | joint_st_return ⇒ 〈required, generated''〉 (* dpm: correct? *)
    106     | joint_st_goto l ⇒
    107       let required' ≝
    108         if marked l visited' then
    109          require l required
    110         else
    111          required
    112       in
    113         if marked l visited' then
    114           〈required', joint_st_goto … globals l :: generated''〉
    115         else
    116           visit globals g required' visited' generated'' l n'
    117     | joint_st_extension ext ⇒ 〈required, generated〉
    118     ]
    119   ]
    120 ].
     28    if set_member … (word_of_identifier … l) visited then
     29     〈set_insert ? (word_of_identifier ? l) required, joint_st_goto … globals l :: generated〉
     30    else
     31     let visited' ≝ set_insert ? (word_of_identifier ? l) visited in
     32     match lookup LabelTag ? g (an_identifier LabelTag (word_of_identifier … l)) with
     33     [ None ⇒ ⊥ (* Case to be made impossible with more dependent types *)
     34     | Some statement ⇒
     35       let translated_statement ≝ translate_statement globals statement in
     36       let generated' ≝ translated_statement :: generated in
     37       match statement with
     38       [ joint_st_sequential instr l2 ⇒
     39         match instr with
     40         [ joint_instr_cond acc_a_reg l1 ⇒
     41            let 〈required', generated''〉 ≝
     42             visit globals g required visited' generated' l2 n' in
     43            let required'' ≝ set_insert ? (word_of_identifier ? l1) required' in
     44             if set_member … (word_of_identifier … l1) visited' then
     45               〈required', generated''〉
     46             else
     47               visit globals g required'' visited' generated'' l1 n'
     48         | _ ⇒ visit globals g required visited' generated' l2 n']
     49     | joint_st_return ⇒ 〈required, generated'〉
     50     | joint_st_goto l2 ⇒ visit globals g required visited' generated' l2 n'
     51     | joint_st_extension ext ⇒ ⊥ ]]].
     52[3: @ext
     53|1,2: @daemon (*CSC: impossible cases, use more dependent types *) ]
     54qed.
    12155
    122 (*
     56(* CSC: The branch compression (aka tunneling) optimization is not implemented
     57   in Matita *)
     58definition branch_compress ≝ λglobals.λa:graph (ltl_statement globals).a.
     59
    12360definition translate_graph ≝
    12461  λglobals: list Identifier.
    125   λg: LTLStatementGraph globals.
    126   λentry: Identifier.
     62  λg: graph (ltl_statement globals).
     63  λentry: label.
     64    let g ≝ branch_compress ? g in
    12765    let visited ≝ set_empty ? in
    128     let required ≝ set_insert ? entry (set_empty ?) in
     66    let required ≝ set_insert ? (word_of_identifier … entry) (set_empty ?) in
    12967    let 〈required', translated〉 ≝ visit globals g required visited [ ] entry in
    13068    let reversed ≝ rev ? translated in
    13169      filter (λs: PreLINStatement globals. ?) reversed.
    132 *)
Note: See TracChangeset for help on using the changeset viewer.