Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
10
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Open sidebar
Vedant Chavda
PROSA - Formally Proven Schedulability Analysis
Commits
4e9768b1
Commit
4e9768b1
authored
Nov 22, 2019
by
Björn Brandenburg
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
model reorg: task.sequential -> task.sequentiality
The property is a noun: a model of task sequentiality.
parent
572c699b
Changes
4
Hide whitespace changes
Inline
Side-by-side
Showing
4 changed files
with
3 additions
and
3 deletions
+3
-3
restructuring/analysis/abstract/core/abstract_seq_rta.v
restructuring/analysis/abstract/core/abstract_seq_rta.v
+1
-1
restructuring/analysis/abstract/instantiations/ideal_processor.v
...turing/analysis/abstract/instantiations/ideal_processor.v
+1
-1
restructuring/analysis/basic_facts/sequential.v
restructuring/analysis/basic_facts/sequential.v
+1
-1
restructuring/model/task/sequentiality.v
restructuring/model/task/sequentiality.v
+0
-0
No files found.
restructuring/analysis/abstract/core/abstract_seq_rta.v
View file @
4e9768b1
...
...
@@ -9,7 +9,7 @@ Require Import rt.restructuring.model.task.preemption.parameters.
Require
Import
rt
.
restructuring
.
analysis
.
basic_facts
.
preemption
.
rtc_threshold
.
job_preemptable
.
Require
Import
rt
.
restructuring
.
model
.
arrival
.
arrival_curves
.
Require
Import
rt
.
restructuring
.
model
.
task
.
sequential
.
Require
Import
rt
.
restructuring
.
model
.
task
.
sequential
ity
.
Require
Import
rt
.
restructuring
.
analysis
.
schedulability
.
Require
Import
rt
.
restructuring
.
analysis
.
basic_facts
.
ideal_schedule
.
Require
Import
rt
.
restructuring
.
analysis
.
basic_facts
.
workload
.
...
...
restructuring/analysis/abstract/instantiations/ideal_processor.v
View file @
4e9768b1
...
...
@@ -2,7 +2,7 @@ Require Export rt.restructuring.analysis.definitions.job_properties.
Require
Export
rt
.
restructuring
.
model
.
task
.
concept
.
Require
Export
rt
.
restructuring
.
model
.
aggregate
.
workload
.
Require
Import
rt
.
restructuring
.
model
.
schedule
.
work_conserving
.
Require
Import
rt
.
restructuring
.
model
.
task
.
sequential
.
Require
Import
rt
.
restructuring
.
model
.
task
.
sequential
ity
.
Require
Import
rt
.
restructuring
.
model
.
priority
.
classes
.
Require
Import
rt
.
restructuring
.
analysis
.
definitions
.
busy_interval
.
Require
Import
rt
.
restructuring
.
analysis
.
definitions
.
priority_inversion
.
...
...
restructuring/analysis/basic_facts/sequential.v
View file @
4e9768b1
Require
Export
rt
.
restructuring
.
model
.
task
.
sequential
.
Require
Export
rt
.
restructuring
.
model
.
task
.
sequential
ity
.
Section
ExecutionOrder
.
(** Consider any type of job associated with any type of tasks... *)
...
...
restructuring/model/task/sequential.v
→
restructuring/model/task/sequential
ity
.v
View file @
4e9768b1
File moved
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