Commit 030af432 authored by Björn Brandenburg's avatar Björn Brandenburg

prosa classic: move import out of section to fix warning

parent 60286128
......@@ -3,6 +3,10 @@ Require Import prosa.classic.model.arrival.basic.job.
Require Import prosa.classic.model.schedule.uni.service
prosa.classic.model.schedule.uni.schedule.
(* Let's import definition of nonpreemptive schedule. *)
Require Import prosa.classic.model.schedule.uni.nonpreemptive.schedule.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
(* In this file, we provide additional definitions and
......@@ -132,9 +136,6 @@ From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
(* In fully nonpreemptive model any job becomes nonpreemptive as soon as it receives one unit of service. *)
Let job_lock_in_service (j: Job) := ε.
(* Let's import definition of nonpreemptive schedule. *)
Require Import prosa.classic.model.schedule.uni.nonpreemptive.schedule.
(* Next, we assume that the schedule is fully nonpreemptive. *)
Hypothesis H_is_nonpreemptive_schedule:
NonpreemptiveSchedule.is_nonpreemptive_schedule job_cost sched.
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment