From cf592e2c777ce7caedcabd23be87e3514c4555d1 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Mon, 30 Dec 2013 12:20:28 +0100 Subject: [PATCH] Automaton module, for finite automata --- _oasis | 2 +- automaton.ml | 133 ++++++++++++++++++++++++++++++++++++++++++++++++++ automaton.mli | 78 +++++++++++++++++++++++++++++ 3 files changed, 212 insertions(+), 1 deletion(-) create mode 100644 automaton.ml create mode 100644 automaton.mli diff --git a/_oasis b/_oasis index 4f4308b9..b7c9bd46 100644 --- a/_oasis +++ b/_oasis @@ -40,7 +40,7 @@ Library "containers" Vector, Bij, PiCalculus, Bencode, Sexp, RAL, MultiSet, UnionFind, SmallSet, Leftistheap, AbsSet, CSM, MultiMap, ActionMan, BV, QCheck, BencodeOnDisk, Show, TTree, - HGraph + HGraph, Automaton BuildDepends: unix Library "containers_thread" diff --git a/automaton.ml b/automaton.ml new file mode 100644 index 00000000..e40d00ee --- /dev/null +++ b/automaton.ml @@ -0,0 +1,133 @@ + +(* +copyright (c) 2013, simon cruanes +all rights reserved. + +redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are met: + +redistributions of source code must retain the above copyright notice, this +list of conditions and the following disclaimer. redistributions in binary +form must reproduce the above copyright notice, this list of conditions and the +following disclaimer in the documentation and/or other materials provided with +the distribution. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND +ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED +WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE +DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE +FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL +DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR +SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER +CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, +OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE +OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. +*) + +(** {1 Distributed Algorithms} *) + +type ('s, -'i, +'o) t = 's -> 'i -> 's * 'o list +(** Transition function of an event automaton *) + +module EventQueue = struct + type t = (unit -> unit) Queue.t + + let create () = Queue.create () + + let default = create () + + let _process q = + while not (Queue.is_empty q) do + let task = Queue.pop q in + task () + done + + let _schedule q task = Queue.push task q +end + +(* empty callback *) +let __noop s i os = true + +type ('s, 'i, 'o) instance = { + transition : ('s, 'i, 'o) t; + queue : EventQueue.t; + mutable state : 's; + mutable connections : 'o connection list; + mutable n_callback : int; + mutable callback : ('s -> 'i -> 's * 'o list -> bool) array; +} + +(* connection to another automaton *) +and 'a connection = Conn : (_, 'a, _) instance -> 'a connection + +let instantiate ?(queue=EventQueue.default) ~f init = { + transition = f; + queue; + state = init; + connections = []; + n_callback = 0; + callback = Array.make 3 __noop; +} + +let transition a i = a.transition a.state i + +let state a = a.state + +(* register a new callback *) +let on_transition a k = + if Array.length a.callback = a.n_callback + then begin + let callback' = Array.make (2 * a.n_callback) __noop in + Array.blit a.callback 0 callback' 0 a.n_callback; + a.callback <- callback'; + end; + a.callback.(a.n_callback) <- k; + a.n_callback <- a.n_callback + 1 + +let connect ~left ~right = + left.connections <- (Conn right) :: left.connections + +(* remove i-th callback of [a] *) +let _remove_callback a i = + if i < a.n_callback + then a.callback.(i) <- a.callback.(a.n_callback - 1); + (* avoid memleak *) + a.callback.(a.n_callback - 1) <- __noop; + a.n_callback <- a.n_callback - 1 + +(* process callback at index [n] *) +let rec _call_callbacks a n s i o = + if n >= a.n_callback then () + else try + let keep = a.callback.(n) s i o in + if keep + then _call_callbacks a (n+1) s i o + else begin + _remove_callback a n; + _call_callbacks a n s i o (* same index, the callback has been removed *) + end + with _ -> _call_callbacks a (n+1) s i o + +(* send input to automaton *) +let rec send : type s i o. (s, i, o) instance -> i -> unit += fun a i -> + let first = Queue.is_empty a.queue in + (* compute transitions *) + let s = a.state in + let s', os = a.transition a.state i in + a.state <- s'; + (* callbacks *) + _call_callbacks a 0 s i (s', os); + (* connections to other automata *) + List.iter + (fun o -> _forward_connections a.connections o) + os; + (* if no enclosing call to [send], we need to process events *) + if first then EventQueue._process a.queue + +and _forward_connections : type a. a connection list -> a -> unit += fun l o -> match l with + | [] -> () + | (Conn a') :: l' -> + EventQueue._schedule a'.queue (fun () -> send a' o); + _forward_connections l' o diff --git a/automaton.mli b/automaton.mli new file mode 100644 index 00000000..a2862039 --- /dev/null +++ b/automaton.mli @@ -0,0 +1,78 @@ + +(* +copyright (c) 2013, simon cruanes +all rights reserved. + +redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are met: + +redistributions of source code must retain the above copyright notice, this +list of conditions and the following disclaimer. redistributions in binary +form must reproduce the above copyright notice, this list of conditions and the +following disclaimer in the documentation and/or other materials provided with +the distribution. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND +ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED +WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE +DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE +FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL +DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR +SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER +CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, +OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE +OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. +*) + +(** {1 Distributed Algorithms} *) + +type ('s, -'i, +'o) t = 's -> 'i -> 's * 'o list +(** Transition function of an event automaton *) + +type ('s, 'i, 'o) instance +(** Instance of an automaton, with a concrete state, and connections to other + automaton instances. *) + +module EventQueue : sig + type t + (** Stateful value used to store the event (pending transitions) that remain + * to process, using an in-memory queue and processing pending tasks until + * none remains. A default global queue is provided, see {!default}. *) + + val default : t + (** Default event queue *) + + val create : unit -> t +end + +val instantiate : ?queue:EventQueue.t -> + f:('s, 'i, 'o) t -> 's -> ('s, 'i, 'o) instance +(** [instantiate ~f init] creates an instance of [f] with initial state + [init]. The [queue] is used to process transitions of this automaton. + + @param queue event queue used to process transitions of the automaton + upon calls to {!send}. Default value is {!EventQueue.default}. *) + +val transition : ('s, 'i, 'o) instance -> 'i -> ('s * 'o list) +(** Compute the transition function for the given input *) + +val state : ('s, _, _) instance -> 's +(** Current state of the automaton instance *) + +val on_transition : ('s, 'i, 'o) instance -> ('s -> 'i -> 's * 'o list -> bool) -> unit +(** [on_state_change a k] calls [k] with the previous state, input, + new state and ouputs of [a] every time [a] changes state. + The callback [k] returns a boolean to signal whether it wants to continue + being called ([true]) or stop being called ([false]). *) + +val connect : left:(_, _, 'a) instance -> right:(_, 'a, _) instance -> unit +(** [connect ~left ~right] connects the ouput of [left] to the input of [right]. + Outputs of [left] will be fed to [right]. *) + +val send : (_, 'i, _) instance -> 'i -> unit +(** [send a i] uses [a]'s transition function to update [a] with the input + event [i]. The output of the transition function (a list of outputs) is + recursively processed. + + This may not terminate, if the automata keep on creating new outputs that + trigger other outputs forever. *)