Probabilistic Schedule

Schedule is a function that maps a time instant to a processor state PState. A probabilistic schedule is a random variable with a codomain in schedules. It is required by the coq-proba library that codomain is an eqType; however, a schedule is a function, which means that there is no decidable equality defined on schedules. We resolve this issue by using a wrapper `{classic _}` that uses axioms of classical logic to make any equality decidable. In addition, note that even though we introduce a horizon after which a system under analysis is terminated, it does not change the type of the scheduler. The point is that the horizon is introduced as an additional parameter to some of the definitions and does not change the type of the scheduler (nat → PState).