reorganize arrival model conversions

- move all to `prosa.model.task.arrival` - unify names to `${FOO}_as_${BAR}.v`

reorganize arrival model conversions
- move all to `prosa.model.task.arrival` - unify names to `${FOO}_as_${BAR}.v`
fb114469 · Björn Brandenburg · 26911c64 · fb114469 · fb114469 · fb114469
Commit fb114469 authored 2 years ago by Björn Brandenburg
--- a/analysis/facts/periodic/arrival_separation.v
+++ b/analysis/facts/periodic/arrival_separation.v
-Require Export prosa.analysis.facts.periodic.sporadic.
+Require Export prosa.model.task.arrival.periodic_as_sporadic.
 Require Export prosa.analysis.facts.sporadic.arrival_times.

 (** In this section we show that the separation between job 

--- a/analysis/facts/periodic/arrival_times.v
+++ b/analysis/facts/periodic/arrival_times.v
+Require Export prosa.model.task.arrival.periodic_as_sporadic.
 Require Export prosa.analysis.facts.periodic.max_inter_arrival.
 Require Export prosa.analysis.facts.model.offset.
-Require Export prosa.analysis.facts.periodic.sporadic.

 (** In this module, we'll prove the known arrival
    times of jobs that stem from periodic tasks. *)

--- a/model/task/arrival/arrival_curve_to_rbf.v
+++ b/model/task/arrival/arrival_curve_to_rbf.v
--- a/analysis/facts/periodic/sporadic.v
+++ b/analysis/facts/periodic/sporadic.v
--- a/model/task/arrival/sporadic_to_arrival_curve.v
+++ b/model/task/arrival/sporadic_to_arrival_curve.v