Changeset 2760 for src/RTLabs


Ignore:
Timestamp:
Mar 2, 2013, 1:29:41 AM (7 years ago)
Author:
sacerdot
Message:
  1. Many files repaired.
  2. 3 new daemons: 2 in Assembly.ma, 1 in StructuredTraces?.ma
Location:
src/RTLabs
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/MeasurableTraces.ma

    r2601 r2760  
    66  RTLabs_fullexec
    77  (λ_.RTLabs_cost)
    8   (λ_. RTLabs_classify).
     8  (λ_. RTLabs_classify) ?.
    99
    1010notation "hbox(‘ ident i ’)" non associative with precedence 90 for @{ (let (${ident i} : unit) ≝ it in ?) }.
  • src/RTLabs/RTLabs_traces.ma

    r2757 r2760  
    22712271#ge #pre #post #CL #ret #callee #AF
    22722272cases pre in CL AF ⊢ %;
    2273 * [ #f #fs #m #S #M #CL @⊥ whd in CL; whd in CL:(??%?); whd in CL:(??(??%)?);
     2273* [ #f #fs #m #S #M #CL @⊥ whd in CL; whd in CL:(??%?); whd in CL:(??%?);
    22742274    cases (next_instruction f) in CL;
    22752275    normalize #A try #B try #C try #D try #E try #F try #G try #H try #J destruct
     
    25082508#ge #flX #s1X #s2X *
    25092509[ #s1 #s2 #EX *
    2510   [ whd in ⊢ (% → ?); #CL #CS #CL' @⊥  change with (Some ? (RTLabs_classify (Ras_state ? s1)) = ?) in CL; >CL' in CL; #CL destruct
     2510  [ whd in ⊢ (% → ?); #CL #CS #CL' @⊥  change with (RTLabs_classify (Ras_state ? s1) = ?) in CL; >CL' in CL; #CL destruct
    25112511  | #CL #CS #CL' @eq_true_to_b @memb_hd
    25122512  ]
    2513 | #s1 #s2 #EX #CL whd in CL; #CL' @⊥ change with (Some ? (RTLabs_classify (Ras_state ? s1)) = ?) in CL; >CL' in CL; #CL destruct
    2514 | #s1 #s2 #s3 #EX #CL #AF #tlr #CS #CL' @⊥ change with (Some ? (RTLabs_classify (Ras_state ? s1)) = ?) in CL; >CL' in CL; #CL destruct
     2513| #s1 #s2 #EX #CL whd in CL; #CL' @⊥ change with (RTLabs_classify (Ras_state ? s1) = ?) in CL; >CL' in CL; #CL destruct
     2514| #s1 #s2 #s3 #EX #CL #AF #tlr #CS #CL' @⊥ change with (RTLabs_classify (Ras_state ? s1) = ?) in CL; >CL' in CL; #CL destruct
    25152515| #s1 #s2 #s3 #EX #CL @⊥ @(RTLabs_notail' … CL)
    2516 | #fl #s1 #s2 #s3 #s4 #EX #CL #AF #tlr #CS #tal #CL' @⊥ change with (Some ? (RTLabs_classify (Ras_state ? s1)) = ?) in CL; >CL' in CL; #CL destruct
     2516| #fl #s1 #s2 #s3 #s4 #EX #CL #AF #tlr #CS #tal #CL' @⊥ change with (RTLabs_classify (Ras_state ? s1) = ?) in CL; >CL' in CL; #CL destruct
    25172517| #fl #s1 #s2 #s3 #EX #tal #CL #CS #CL' @eq_true_to_b @memb_hd
    25182518] qed.
     
    27702770| @no_loops_in_tal // @simplify_cl @CL
    27712771] qed.
    2772 
Note: See TracChangeset for help on using the changeset viewer.