eval_event_model.v 768 Bytes
Newer Older
Pascal Fradet's avatar
Pascal Fradet committed
1 2 3 4
Require Import Arith NPeano List Omega.

Require Import event_model types. 

lina marsso's avatar
lina marsso committed
5 6
(* ########################################################### *)
(** *          Evaluations                                     *)
Pascal Fradet's avatar
Pascal Fradet committed
7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36
(* ########################################################### *)

Definition sigma (t : instant) : nb_occurrences :=
match t with
  | 0 => 0
  | 1 => 0
  | 2 => 1
  | 3 => 2
  | 4 => 0
  | 5 => 0
  | 6 => 3
  | n => 1
 end.


(*
Example test_delta : @delta sigma1 AE 1 3 = 1.
unfold delta.
simpl.
unfold instant_of.
assert (H : instant_after sigma1 AE 3 0 = 3).
 - 
   unfold instant_after.
   elim sigma1.
   induction sigma1.
   unfold instant_after_func.
   simpl.
   induction.
Eval compute in (@next sigma1 AE 1).

lina marsso's avatar
lina marsso committed
37
*)