Commit 574dcc47 authored by jonathan julou's avatar jonathan julou

changed a name

parent 807901f6
Pipeline #19264 failed with stages
in 3 minutes and 45 seconds
......@@ -4,7 +4,7 @@ From rt.restructuring.model Require Export preemptive.
From rt.restructuring.model Require Export work_conserving.
From rt.restructuring.analysis Require Export schedulability_up_to_t.
(*From rt.restructuring.implementation Require Export prefix.*)
From rt.restructuring.implementation Require Export prefix.
Set Bullet Behavior "Strict Subproofs".
......@@ -218,10 +218,22 @@ Section Transformation.
Definition arr_seq_prefixed time:=
if ( time <= t ) then ( arr_seq time ) else ( nil ).
(*
Definition complete_schedule : schedule State :=
fun t => complete_schedule_helper (t - t_start) t.
*)
(* [next_state t candidate_jobs] should return the schedule state at time t given the list of pending jobs and their remaining cost *)
Variable next_state : instant -> seq (Jobs * duration) -> State.
Variable t_start : instant.
Hypothesis next_state_correct : forall t jobs j,
scheduled_in j (next_state t jobs) -> j \in map fst jobs.
Hypothesis next_state_service : forall t jobs j c,
(j, c) \in jobs -> service_in j (next_state t jobs) <= c.
Definition sched_prefixed := complete_schedule arr_seq next_state sched t.
Check sched_prefixed.
Lemma valid_arrival_sequence_completion :
valid_arrival_sequence_up_to_t arr_seq t ->
valid_arrival_sequence arr_seq_prefixed.
......
......@@ -706,7 +706,7 @@ Section PathResponseTime.
(* --- XV --- PARTICULARISED MAIN RESULT --- XV --- *)
(*========================================================================*)
Lemma main_lemma : valid_functional_path_response_time_bound PRT.
Lemma functionnal_path_valid_latency : valid_functional_path_response_time_bound PRT.
Proof.
unfold valid_functional_path_response_time_bound.
intros j in_task in_arr_seq.
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment