Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
R
rt-proofs
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
0
Issues
0
List
Boards
Labels
Service Desk
Milestones
Merge Requests
1
Merge Requests
1
CI / CD
CI / CD
Pipelines
Jobs
Schedules
Operations
Operations
Incidents
Environments
Analytics
Analytics
CI / CD
Repository
Value Stream
Wiki
Wiki
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Jobs
Commits
Issue Boards
Open sidebar
Sergey Bozhko
rt-proofs
Commits
45853287
Commit
45853287
authored
Jun 04, 2019
by
Maxime Lesourd
Committed by
Björn Brandenburg
Jun 05, 2019
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
applied naming convention to behavior
parent
557ced9d
Changes
3
Hide whitespace changes
Inline
Side-by-side
Showing
3 changed files
with
12 additions
and
12 deletions
+12
-12
restructuring/behavior/arrival/arrival_sequence.v
restructuring/behavior/arrival/arrival_sequence.v
+4
-4
restructuring/behavior/facts/arrivals.v
restructuring/behavior/facts/arrivals.v
+7
-7
restructuring/behavior/schedule/schedule.v
restructuring/behavior/schedule/schedule.v
+1
-1
No files found.
restructuring/behavior/arrival/arrival_sequence.v
View file @
45853287
...
...
@@ -51,18 +51,18 @@ Section ValidArrivalSequence.
(* We say that arrival times are consistent if any job that arrives in the
sequence has the corresponding arrival time. *)
Definition
arrival_times_are_consistent
:
=
Definition
consistent_arrival_times
:
=
forall
j
t
,
arrives_at
arr_seq
j
t
->
job_arrival
j
=
t
.
(* We say that the arrival sequence is a set iff it doesn't contain duplicate
jobs at any given time. *)
Definition
arrival_sequence_
is_a_set
:
=
forall
t
,
uniq
(
jobs_arriving_at
arr_seq
t
).
Definition
arrival_sequence_
uniq
:
=
forall
t
,
uniq
(
jobs_arriving_at
arr_seq
t
).
(* We say that the arrival sequence is valid iff it is a set and arrival times
are consistent *)
Definition
arrival_sequence_is_valid
:
=
arrival_times_are_consistent
/\
arrival_sequence_is_a_set
.
Definition
valid_arrival_sequence
:
=
consistent_arrival_times
/\
arrival_sequence_uniq
.
End
ValidArrivalSequence
.
...
...
restructuring/behavior/facts/arrivals.v
View file @
45853287
...
...
@@ -78,8 +78,8 @@ Section ArrivalSequencePrefix.
Section
ArrivalTimes
.
(* Assume that job arrival times are consistent. *)
Hypothesis
H_
arrival_times_are_consistent
:
arrival_times_are_consistent
arr_seq
.
Hypothesis
H_
consistent_arrival_times
:
consistent_arrival_times
arr_seq
.
(* First, we prove that if a job belongs to the prefix
(jobs_arrived_before t), then it arrives in the arrival sequence. *)
...
...
@@ -88,7 +88,7 @@ Section ArrivalSequencePrefix.
j
\
in
jobs_arrived_between
t1
t2
->
arrives_in
arr_seq
j
.
Proof
.
rename
H_
arrival_times_are_consistent
into
CONS
.
rename
H_
consistent_arrival_times
into
CONS
.
intros
j
t1
t2
IN
.
apply
mem_bigcat_nat_exists
in
IN
.
move
:
IN
=>
[
arr
[
IN
_
]].
...
...
@@ -103,7 +103,7 @@ Section ArrivalSequencePrefix.
j
\
in
jobs_arrived_between
t1
t2
->
arrived_between
j
t1
t2
.
Proof
.
rename
H_
arrival_times_are_consistent
into
CONS
.
rename
H_
consistent_arrival_times
into
CONS
.
intros
j
t1
t2
IN
.
apply
mem_bigcat_nat_exists
in
IN
.
move
:
IN
=>
[
t0
[
IN
/=
LT
]].
...
...
@@ -131,7 +131,7 @@ Section ArrivalSequencePrefix.
arrived_between
j
t1
t2
->
j
\
in
jobs_arrived_between
t1
t2
.
Proof
.
rename
H_
arrival_times_are_consistent
into
CONS
.
rename
H_
consistent_arrival_times
into
CONS
.
move
=>
j
t1
t2
[
a_j
ARRj
]
BEFORE
.
have
SAME
:
=
ARRj
;
apply
CONS
in
SAME
;
subst
a_j
.
by
apply
mem_bigcat_nat
with
(
j
:
=
(
job_arrival
j
)).
...
...
@@ -140,10 +140,10 @@ Section ArrivalSequencePrefix.
(* Next, we prove that if the arrival sequence doesn't contain duplicate
jobs, the same applies for any of its prefixes. *)
Lemma
arrivals_uniq
:
arrival_sequence_
is_a_set
arr_seq
->
arrival_sequence_
uniq
arr_seq
->
forall
t1
t2
,
uniq
(
jobs_arrived_between
t1
t2
).
Proof
.
rename
H_
arrival_times_are_consistent
into
CONS
.
rename
H_
consistent_arrival_times
into
CONS
.
unfold
jobs_arrived_up_to
;
intros
SET
t1
t2
.
apply
bigcat_nat_uniq
;
first
by
done
.
intros
x
t
t'
IN1
IN2
.
...
...
restructuring/behavior/schedule/schedule.v
View file @
45853287
...
...
@@ -85,7 +85,7 @@ Section Schedule.
(* We say that the schedule is valid iff
- jobs come from some arrival sequence
- a job can only be scheduled if it has arrived and is not completed yet *)
Definition
schedule_is_valid
(
arr_seq
:
arrival_sequence
Job
)
:
=
Definition
valid_schedule
(
arr_seq
:
arrival_sequence
Job
)
:
=
jobs_come_from_arrival_sequence
arr_seq
/\
jobs_must_arrive_to_execute
/\
completed_jobs_dont_execute
.
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment