package rfsm

  1. Overview
  2. Docs
A toolset for describing and simulating StateChart-like state diagrams

Install 

dune-project
 Dependency

github.com Readme Changelog Edit opam file Versions (8)

Authors

  1. J
    Jocelyn Sérot <jocelyn.serot@uca.fr>

Maintainers

  1. J
    Jocelyn Sérot <jocelyn.serot@uca.fr>

Sources

2.2.tar.gz
md5=ea1b496f0aa758933ae23921ee55a531
sha512=4fa72747bb2e32f91d64e4b8c24f60d6f0bdad297cc40f36d5c687ed1de900ab8441fa8a12aecf2523928833cddd5391fa87c11a1af2162ac8001467e8f485a5

doc/src/rfsm/evseq.ml.html

Source file evseq.ml

1
2
3
4
5
6
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
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
(**********************************************************************)
(*                                                                    *)
(*              This file is part of the RFSM package                 *)
(*                                                                    *)
(*  Copyright (c) 2018-present, Jocelyn SEROT.  All rights reserved.  *)
(*                                                                    *)
(*  This source code is licensed under the license found in the       *)
(*  LICENSE file in the root directory of this source tree.           *)
(*                                                                    *)
(**********************************************************************)

(**{1 Event sequences} *)

(** An {e event sequence} is a sequence of dated event sets. Ex: [[{H,x<-1}@t=10; {H}@t=20, ...]].
    Event sequences are to describe both {e stimuli} and {e responses}. *)

module type EVSEQ = sig
  
  module Evset: Evset.T

  type t = Evset.t list
  type value

  val merge: t -> t -> t
  val (@@) : t -> t -> t  (** [@@] is the infix notation for [merge] *)

  val merge_all: t list -> t 
  
  val mk_periodic: Ident.t -> int -> int -> int -> t
  val mk_changes: Ident.t -> (int * value) list -> t
  val mk_sporadic: Ident.t -> int list -> t
    
  val pp: Format.formatter -> t -> unit

end
 
module Make (ES: Evset.T) : EVSEQ with module Evset = ES and type value = ES.Event.Value.t =
struct
  module Evset = ES

  type value = Evset.Event.Value.t
             
  type t = Evset.t list

  let rec merge st1 st2 =
    match st1, st2 with
    | [], _ -> st2
    | _, [] -> st1
    | evs1::rest1, evs2::rest2 ->
       let t1 = Evset.date evs1 in
       let t2 = Evset.date evs2 in
       if t1=t2 then (Evset.union evs1 evs2) :: merge rest1 rest2
       else if t1<t2 then evs1 :: merge rest1 st2
       else (* t1 > t2 *) evs2 :: merge st1 rest2
  
  let (@@) = merge
  
  let merge_all sts = List.fold_left merge [] sts
  
  let mk_periodic name p t1 t2 =
    let rec mk t =
      if t <= t2 then Evset.mk t [Evset.Event.Ev name] :: mk (t+p)
      else [] in
    mk t1
  
  let mk_changes name tvs =
    let open Evset.Event in
    List.map (fun (t,v) -> Evset.mk t [Upd (Syntax.mk_simple_lval name, v)]) tvs
  
  let mk_sporadic name ts =
    List.map (fun t -> Evset.mk t [Evset.Event.Ev name]) ts
    
  let pp fmt es = 
    Ext.List.pp_v Evset.pp fmt es

end