Compare revisions

a162d510 · a162d510 · a162d510 · a162d510 · a162d510 · a162d510
--- a/analysis/definitions/blocking_bound/fp.v
+++ b/analysis/definitions/blocking_bound/fp.v
--- a/analysis/definitions/busy_interval/classical.v
+++ b/analysis/definitions/busy_interval/classical.v
--- a/analysis/definitions/busy_interval/edf_pi_bound.v
+++ b/analysis/definitions/busy_interval/edf_pi_bound.v
--- a/analysis/definitions/carry_in.v
+++ b/analysis/definitions/carry_in.v
--- a/analysis/definitions/completion_sequence.v
+++ b/analysis/definitions/completion_sequence.v
--- a/analysis/definitions/delay_propagation.v
+++ b/analysis/definitions/delay_propagation.v
--- a/analysis/definitions/demand_bound_function.v
+++ b/analysis/definitions/demand_bound_function.v
--- a/analysis/definitions/finish_time.v
+++ b/analysis/definitions/finish_time.v
--- a/analysis/definitions/hyperperiod.v
+++ b/analysis/definitions/hyperperiod.v
--- a/analysis/definitions/infinite_jobs.v
+++ b/analysis/definitions/infinite_jobs.v
--- a/analysis/definitions/interference.v
+++ b/analysis/definitions/interference.v
--- a/analysis/definitions/job_properties.v
+++ b/analysis/definitions/job_properties.v
+Require Export prosa.behavior.all.
+
+(** In this section, we introduce properties of a job. *)
+Section PropertiesOfJob.
+
+  (** Assume that job costs are known. *)
+  Context {Job : JobType}.
+  Context `{JobCost Job}.
+
+  (** Consider an arbitrary job. *)
+  Variable j : Job.
+
+  (** The job cost must be positive. *)
+  Definition job_cost_positive := job_cost j > 0.
+
+End PropertiesOfJob. 
\ No newline at end of file
--- a/analysis/definitions/job_response_time.v
+++ b/analysis/definitions/job_response_time.v
--- a/analysis/definitions/priority/classes.v
+++ b/analysis/definitions/priority/classes.v
--- a/analysis/definitions/priority_inversion.v
+++ b/analysis/definitions/priority_inversion.v
--- a/analysis/definitions/progress.v
+++ b/analysis/definitions/progress.v
--- a/analysis/definitions/readiness.v
+++ b/analysis/definitions/readiness.v
--- a/analysis/definitions/request_bound_function.v
+++ b/analysis/definitions/request_bound_function.v
--- a/analysis/definitions/sbf/busy.v
+++ b/analysis/definitions/sbf/busy.v
--- a/analysis/definitions/sbf/plain.v
+++ b/analysis/definitions/sbf/plain.v
No results found