A dumbest implementation for LTL ( see http://www.cds.caltech.edu/~murray/courses/afrl-sp12/L3_ltl-24Apr12.pdf )

dumbest_ltl.ml

type prop =
 True |
 Var of char |
 And of prop * prop |
 Not of prop |
 N of prop |
 U of prop * prop

(* slow! *)
let eventually p = U (True, p)
let always p = Not (eventually (Not p))

let rec check prop seq t =
  match prop with
  | True -> true
  | Var c -> List.assoc c (List.nth seq t)
  | And (a, b) -> check a seq t && check b seq t
  | Not p -> not (check p seq t)
  | N p -> if t + 1 < List.length seq then check p seq (t + 1) else false
  | U (a, b) -> if check b seq t then true else
                  if check a seq t && t + 1 < List.length seq
                    then check (U (a, b)) seq (t + 1)
                    else false

let test1 = check (Var 'a') [[('a', true)]; [('a', false)]] 0
let test2 = check (N (Var 'a')) [[('a', false)]; [('a', true)]] 0
let test3 = check (U (Var 'a', Var 'b'))
              [[('a', true); ('b', false)];
               [('a', true); ('b', false)];
               [('a', true); ('b', false)];
               [('a', true); ('b', false)];
               [('a', false); ('b', true)]] 0
let test4_1 = check (eventually (Var 'a'))
              [[('a', false)]; [('a', false)]; [('a', false)]; [('a', true)]] 0
let test4_2 = check (eventually (Var 'a'))
              [[('a', false)]; [('a', false)]; [('a', false)]] 0
let test5_1 = check (always (Var 'a'))
              [[('a', true)]; [('a', true)]; [('a', true)]] 0
let test5_2 = check (always (Var 'a'))
              [[('a', true)]; [('a', true)]; [('a', false)]] 0