Implements the Hennessy–Milner logic on OCaml

HML.ml

(*
 * HML.ml
 * This file is part of hml
 *
 * Copyright (C) 2013 - Giacomo Bergami
 *
 * hml is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * hml is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with hml; if not, write to the Free Software
 * Foundation, Inc., 51 Franklin St, Fifth Floor, 
 * Boston, MA  02110-1301  USA
 *)

include List;;

(* Defines an "all" string called Act (the set of all the action of the lts), or a list of strings *)
type strings = 
  | Stri of string list
  | Act



(* HML non recursive Syntax *)
type syntax = 
    True                           (* tt        *)
  | False                          (* ff        *)
  | And of syntax * syntax         (* F ^ G     *)
  | Or of syntax * syntax          (* F v G     *)
  | LDiam of strings * syntax  (* <A,...> F *)
  | LBox of strings * syntax   (* [B,...] F *)
  | Diam of string * syntax        (* <A> F     *)
  | Box of string * syntax         (* [B] F     *)
  | Rec of int                     (* Any Variable *)

(* Selects the minimum or maximum *)
type sol = 
  | MIN | MAX

(* An equation of a system is made of a minimum/maximum solution, and its formula *)
type system = System of sol * syntax
(* A system of formulas is made by a "system list", where the i-th equation could
   use only the results for the former equations (0...i-1) *)

(* Definition of a LTS relation *)
type rel = Rel of int * string * int

(* Definition of a LTS *)
type lts = Lts of (int list * string list * rel list) (** (Q,A,R) **)

(* Casts a list of strings or selects the ACT *)
let getstring  gs qar = 
  match gs with
    | Stri u -> u
    | Act -> match qar with Lts (q,a,r) -> a

(* Appends an element to a list if it's not its member *)
let nmem_app a l = if mem a l then l else a::l

let rec lts_from_rell rel rl = 
  match rel with Lts (l1,l2,l3) ->
  (match rl with
    |  [] -> Lts (sort compare l1, sort compare l2, sort compare l3)
    |  a::b -> (match a with 
                 | Rel (x,y,z) -> 
                         lts_from_rell (Lts ((nmem_app z (nmem_app x l1)), nmem_app y l2, nmem_app a l3))  b         
               )
  )

(* It defines an LTS from a relation list *)
let lts_from_rel rl = lts_from_rell (Lts ([],[],[])) rl


(* Basics of semantix box and diamond semantic funcionts [·_·] and <._.> respectively *)
let bdsem2 op qar a sS  =
                 
match qar with Lts(q,_,r) ->

filter (fun p -> op ((fun xyz -> match xyz with Rel(x,y,z) -> mem z sS))
                    (filter (fun xyz -> match xyz with Rel(x,y,z) -> y=a && x=p) r))
       q

let boxsem2 = bdsem2 for_all
let diasem2 = bdsem2 exists

(*
let mlts = lts_from_rel [Rel (1,"req",2);Rel (2,"a",3);Rel (3,"grant",4)];;
*)

(* Lists intersection *)
let rec intersect l m = 
  match l with
    | [] -> []
    | a::b -> if mem a m then a::(intersect b m) else (intersect b m)

(* Obtains a list of distinct elements *)
let rec distinct l =
   match l with
     | [] -> []
     | a::b -> if mem a b then (distinct b) else a::(distinct b)

(* Semantic Function *)
let rec semantics s qar repo i qset  =
  match qar with Lts (q,a,r) ->
  match s with
    | True -> q
    | False -> []
    | And (c,b) -> distinct (intersect (semantics c qar repo i qset  ) (semantics b qar repo i qset  ))
    | Or (c,b) -> distinct ((semantics c qar repo i qset  )@(semantics b qar repo i qset  ))
    | Diam (a,ss) -> diasem2 qar a (semantics ss qar repo i qset  )
    | Box (a,ss) -> boxsem2 qar a (semantics ss qar repo i qset  )
    | LDiam (ls,ss) -> (match (getstring ls qar) with 
                          | [] -> q
                          | c::[] -> (semantics (Diam (c,ss)) qar repo i qset )
                          | c::b -> distinct ((semantics (Diam (c,ss)) qar repo i qset )@(semantics (LDiam (Stri b,ss)) qar repo i qset )))
    | LBox (ls,ss) -> (match (getstring ls qar) with
                         | [] -> q
                         | c::[] -> (semantics (Box (c,ss)) qar repo i qset )
                         | c::b -> distinct (intersect (semantics (Box (c,ss)) qar repo i qset ) (semantics (LBox (Stri b,ss)) qar repo i qset )))
    | Rec y ->  if (y<i) then nth repo y else qset 


(* Defines the minimization and maximization calculation with Tarski's Method *)
let rec approxim s f i = if (compare s (f s)==0) then (i,s) else approxim (f s) f (i+1)
let min s qar repo i = approxim [] (semantics s qar repo i) 1
let max s qar repo i = match qar with Lts (q,a,r) -> approxim q (semantics s qar repo i) 1

let solve_step_system a b qar repo i = 
    match a with 
      | MIN -> min b qar repo i
      | MAX -> max b qar repo i;;

let rec subst_step prev next qar i = 
  match next with
    | [] -> prev
    | a::b -> match a with System (x,y) -> subst_step (prev@[match solve_step_system x y qar prev i with (ww,yy) -> yy]) b qar (i+1);;


let solve_system sis lts = subst_step [] sis lts 0

(* Some frequently used semantic functions, where i is the number dedicated to the variable *)
let inv i f = System(MAX, And (f,LBox (Act, Rec i)));;
let pos i f = System(MIN, Or  (f,LDiam(Act, Rec i)));;
let even i f = System(MIN, Or (f,And (LDiam (Act, True),LBox (Act, Rec i))));;
let safe i f = System(MAX, And (f,Or (LBox (Act, False),LDiam (Act, Rec i))));;










let mlts1 = lts_from_rel [Rel (0,"t",1);Rel (1,"t",0); Rel(2,"a",1); Rel (2,"a",3)];;
let mlts2 = lts_from_rel [Rel (0,"t",1);Rel (1,"t",0); Rel(2,"a",1); Rel (2,"t",3); Rel (2,"t",2)];;

let mltsg = lts_from_rel [Rel (0,"a",1);Rel (1,"t",1); Rel(1,"t",2); Rel (2,"t",3)];;
let livelock = System(MIN,(Diam ("t",Rec 0)));;

let livelocknow = System(MAX,(Diam("t",Rec 0)));;

let ln = System(MAX,(Diam ("t",Rec 0)));;
let lnm = System(MIN,(Diam ("t",Rec 0)));;
let lng = System(MAX,(Box ("t",Rec 0)));;
let lng2 = System(MIN,(Box ("t",Rec 0)));;
let ln2 = inv 0 (Box ("t",True));;

let poslivelocknow = [livelocknow; pos 1 (Rec 0)];;
let poslivelocknow2 = [lng2; pos 1 (Rec 0)];;
let invlivelocknow = [lnm; inv 1 (Rec 0)];;


solve_system [lnm] mlts1;; (* [[]]        *)
solve_system [lng] mltsg;; (* [[0;1;2;3]] *)
solve_system [ln2] mltsg;; (* [[0;1;2;3]] *)
solve_system poslivelocknow mltsg;;
solve_system poslivelocknow2 mltsg;;
solve_system invlivelocknow mltsg;;

print_string "Now, some real examples\n";;

solve_system [ln] mlts1;;
solve_system [livelocknow] mlts1;;
solve_system poslivelocknow mlts2;;