Skip to content
/ kat Public

Kleene Algebra with Tests (KAT) and Brzozowski automata

License

Notifications You must be signed in to change notification settings

smolkaj/kat

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

7 Commits
 
 
 
 
 
 
 
 

Repository files navigation

Kleene Algebra with Test

Bare-bones implementation of Kleene Algebra with Tests (KAT) and Brzozowski derivatives.

Dependencies

You will need OCaml (tested with 4.07.1) and OPAM (version 2), OCaml's packet manager.

We also use a few libraries and the OCaml build tool "dune"; you can install everything using OPAM as follows:

opam install dune hashcons ppx_jane

Quickstart

You can quickly experiment with the library by install utop,

opam install utop

and then starting an interactive OCaml session with the library loaded, by executing the following from the root of the project:

dune utop .

Execute the following in the utop session:

$ open Kat;;
$ #install_printer ExpACI.pp;;

Then, experiment as you please. For example:

$ let e = Exp.(Star (Union (Seq (Test (Test T1), Seq (Union (Action A1, Action A2), Action A3)), (Seq (Test (Not (Test T2)), Action A2)))));;

$ let dfa = ExpACI.brzozowski_dfa e;;
> val dfa : ExpACI.t dfa =
>   {start = (T1·(A1 + A2)·A3 + ¬T2·A2)*; obs = <fun>; trans = <fun>}

$ let s0 = dfa.start;;
> val s0 : ExpACI.t = (T1·(A1 + A2)·A3 + ¬T2·A2)*

$ let s1 = dfa.trans s0 (function T1 -> true | _ -> false) A2;;
> val s1 : ExpACI.t = (1 + A3)·(T1·(A1 + A2)·A3 + ¬T2·A2)*

$ let s2 = dfa.trans s0 (fun _ -> true) A2;;
> val s2 : ExpACI.t = A3·(T1·(A1 + A2)·A3 + ¬T2·A2)*

Releases

No releases published

Packages

No packages published

Languages