Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Marco Maida
PROSA - Formally Proven Schedulability Analysis
Commits
62c5aa23
Commit
62c5aa23
authored
Oct 30, 2020
by
Marco Maida
🌱
Browse files
Added delta-min theory (to discuss)
parent
109324ac
Pipeline
#36703
failed with stages
in 17 minutes and 5 seconds
Changes
2
Pipelines
1
Expand all
Hide whitespace changes
Inline
Side-by-side
model/task/arrival/curves.v
View file @
62c5aa23
...
...
@@ -28,11 +28,11 @@ Class MinArrivals (Task : TaskType) := min_arrivals : Task -> duration -> nat.
maximum-distance functions. *)
(** We let [min_separation tsk N] denote the minimal length of an interval in
which
exactly
[N] jobs of task [tsk] arrive. *)
which
at least
[N] jobs of task [tsk] arrive. *)
Class
MinSeparation
(
Task
:
TaskType
)
:
=
min_separation
:
Task
->
nat
->
duration
.
(** Conversely, we let [max_separation tsk N] denote the maximal length of an interval in
which
exactly
[N] jobs of task [tsk] arrive. *)
which
at most
[N] jobs of task [tsk] arrive. *)
Class
MaxSeparation
(
Task
:
TaskType
)
:
=
max_separation
:
Task
->
nat
->
duration
.
...
...
model/task/arrival/delta_min.v
0 → 100644
View file @
62c5aa23
This diff is collapsed.
Click to expand it.
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