File ‹code/Autool.sml›

open Complementation
open String
open List

fun eq x y = (x = y)

fun println w = print (w ^ "\n")

fun return x = [x]
fun bind xs f = concat (map f xs)
fun foldl' y f [] = y
  | foldl' y f (x :: xs) = foldl f x xs
fun takeWhile P [] = []
  | takeWhile P (x :: xs) = if P x then x :: takeWhile P xs else []
fun lookup x [] = NONE |
    lookup x ((k, v) :: xs) = if x = k then SOME v else lookup x xs
fun upto k = if k = 0 then [] else (k - 1) :: upto (k - 1)

fun splitFirst u w =
	if w = ""
	then if u = "" then SOME ("", "") else NONE
	else
		if isPrefix u w
		then SOME ("", extract (w, size u, NONE))
		else case splitFirst u (extract (w, 1, NONE)) of
			NONE => NONE |
			SOME (v, w') => SOME (str (sub (w, 0)) ^ v, w')
fun split u w = case splitFirst u w of NONE => [w] | SOME (v, w') => v :: split u w'

fun showInt k = Int.toString k
fun parseInt w = case Int.fromString w of SOME n => n

fun showNat k = showInt (integer_of_nat k)
fun parseNat w = nat_of_integer (parseInt w)

fun showString w = "\"" ^ w ^ "\""
fun parseString w = substring (w, 1, size w - 2)

fun showTuple f g (x, y) = "(" ^ f x ^ ", " ^ g y ^ ")"
fun showSequence f xs = concatWith ", " (map f xs)
fun showList f xs = "[" ^ showSequence f xs ^ "]"
fun showSet f (Set xs) = "{" ^ showSequence f xs ^ "}"
  | showSet f (Coset xs) = "- {" ^ showSequence f xs ^ "}"

fun showFormula f False = "f"
  | showFormula f True = "t"
  | showFormula f (Variable v) = f v
  | showFormula f (Negation x) = "!" ^ showFormula f x
  | showFormula f (Conjunction (x, y)) = "(" ^ showFormula f x ^ " & " ^ showFormula f y ^ ")"
  | showFormula f (Disjunction (x, y)) = "(" ^ showFormula f x ^ " | " ^ showFormula f y ^ ")"
fun parseFormula parseVariable input = let
  fun parseConstant w cs = if isPrefix w (implode cs) then [(w, drop (cs, size w))] else []
  fun parseAtom input1 =
    bind (parseConstant "f" input1) (fn (_, input2) =>
    return (False, input2))
    @
    bind (parseConstant "t" input1) (fn (_, input2) =>
    return (True, input2))
    @
    bind (parseVariable input1) (fn (variable, input2) =>
    return (Variable variable, input2))
    @
    bind (parseConstant "(" input1) (fn (_, input2) =>
    bind (parseDisjunction input2) (fn (disjunction, input3) =>
    bind (parseConstant ")" input3) (fn (_, input4) =>
    return (disjunction, input4))))
  and parseLiteral input1 =
    bind (parseAtom input1) (fn (atom, input2) =>
    return (atom, input2))
    @
    bind (parseConstant "!" input1) (fn (_, input2) =>
    bind (parseAtom input2) (fn (atom, input3) =>
    return (Negation atom, input3)))
  and parseConjunction input1 =
    bind (parseLiteral input1) (fn (literal, input2) =>
    return (literal, input2))
    @
    bind (parseLiteral input1) (fn (literal, input2) =>
    bind (parseConstant "&" input2) (fn (_, input3) =>
    bind (parseConjunction input3) (fn (conjunction, input4) =>
    return (Conjunction (literal, conjunction), input4))))
  and parseDisjunction input1 =
    bind (parseConjunction input1) (fn (conjunction, input2) =>
    return (conjunction, input2))
    @
    bind (parseConjunction input1) (fn (conjunction, input2) =>
    bind (parseConstant "|" input2) (fn (_, input3) =>
    bind (parseDisjunction input3) (fn (disjunction, input4) =>
    return (Disjunction (conjunction, disjunction), input4))))
  val input' = filter (not o Char.isSpace) (explode input)
  val result = map (fn (exp, _) => exp) (filter (fn (exp, rest) => null rest) (parseDisjunction input'))
  in hd result end

datatype hoaProperty =
  HoaVersion of string |
  HoaName of string |
  HoaProperties of string list |
  HoaAtomicPropositions of nat * string list |
  HoaAcceptanceConditionName of string |
  HoaAcceptanceCondition of string |
  HoaStartState of nat |
  HoaStateCount of nat |
  HoaProperty of string * string
datatype hoaTransition = HoaTransition of nat formula * nat
datatype hoaState = HoaState of nat * nat list * hoaTransition list
datatype hoaAutomaton = HoaAutomaton of hoaProperty list * hoaState list

fun showHoaAutomaton (HoaAutomaton (ps, ss)) = let
  fun showProperty (HoaVersion w) = "HOA: " ^ w ^ "\n"
    | showProperty (HoaName w) = "name: " ^ showString w ^ "\n"
    | showProperty (HoaProperties ws) = "properties: " ^ concatWith " " ws ^ "\n"
    | showProperty (HoaAtomicPropositions (n, ps)) = "AP: " ^ showNat n ^ " " ^ concatWith " " (map showString ps) ^ "\n"
    | showProperty (HoaAcceptanceConditionName w) = "acc-name: " ^ w ^ "\n"
    | showProperty (HoaAcceptanceCondition w) = "Acceptance: " ^ w ^ "\n"
    | showProperty (HoaStartState p) = "Start: " ^ showNat p ^ "\n"
    | showProperty (HoaStateCount n) = "States: " ^ showNat n ^ "\n"
    | showProperty (HoaProperty (name, value)) = name ^ ": " ^ value ^ "\n"
  fun showTransition (HoaTransition (a, q)) = "[" ^ showFormula showNat a ^ "]" ^ " " ^ showNat q ^ "\n"
  fun showState (HoaState (p, cs, ts)) = "State: " ^ showNat p ^ " " ^ showSet showNat (Set cs) ^ "\n" ^ String.concat (map showTransition ts)
  in String.concat (map showProperty ps) ^ "--BODY--" ^ "\n" ^ String.concat (map showState ss) ^ "--END--" ^ "\n" end
fun parseHoaAutomaton path = let
  fun parseVariable cs = case takeWhile Char.isDigit cs of
    [] => [] | xs => [(parseNat (implode xs), drop (cs, length xs))]
	fun inputLine input = case TextIO.inputLine input of SOME w => substring (w, 0, size w - 1)
	fun parseProperty w = case split ": " w of
	  ["HOA", u] => HoaVersion u |
	  ["name", u] => HoaName (substring (u, 1, size u - 2)) |
	  ["properties", u] => HoaProperties (split " " u) |
	  ["AP", u] => (case split " " u of v :: vs => HoaAtomicPropositions (parseNat v, map parseString vs)) |
	  ["acc-name", u] => HoaAcceptanceConditionName u |
	  ["Acceptance", u] => HoaAcceptanceCondition u |
	  ["Start", u] => HoaStartState (parseNat u) |
	  ["States", u] => HoaStateCount (parseNat u) |
	  [name, value] => HoaProperty (name, value)
	fun parseProperties input = case inputLine input of w =>
	  if w = "--BODY--" then []
	  else parseProperty w :: parseProperties input
	fun parseTransition w = case split "] " (substring (w, 1, size w - 1)) of
	  [u, v] => HoaTransition (parseFormula parseVariable u, parseNat v)
	fun parseTransitions input = case inputLine input of w =>
	  if isPrefix "State" w orelse w = "--END--" then ([], w)
	  else case parseTransitions input of (ts, w') => (parseTransition w :: ts, w')
	fun parseStateHeader w = case split " {" w of
	  [u] => (parseNat u, []) |
	  [u, "}"] => (parseNat u, []) |
	  [u, v] => (parseNat u, map parseNat (split ", " (substring (v, 0, size v - 1))))
	fun parseState input w =
	  case split ": " w of ["State", u] =>
	  case parseStateHeader u of (p, cs) =>
	  case parseTransitions input of (ts, w') =>
	  (HoaState (p, cs, ts), w')
	fun parseStates input w =
	  if w = "--END--" then []
	  else case parseState input w of (p, w') => p :: parseStates input w'
	val input = TextIO.openIn path
	val properties = parseProperties input
	val states = parseStates input (inputLine input)
	in HoaAutomaton (properties, states) before TextIO.closeIn input end

fun toNbaei (HoaAutomaton (properties, states)) = let
  fun atomicPropositions (HoaAtomicPropositions (_, ps) :: properties) = ps
    | atomicPropositions (_ :: properties) = atomicPropositions properties
  val aps = atomicPropositions properties
  val alphabet = case pow {equal = eq} (Set aps) of Set pps => pps
  fun startStates [] = []
    | startStates (HoaStartState p :: properties) = p :: startStates properties
    | startStates (property :: properties) = startStates properties
  val initial = startStates properties
  fun mapFormula f = map_formula (fn k => nth (aps, integer_of_nat k)) f
  fun expandTransition p f q = map (fn P => (p, (P, q))) (filter (fn x => satisfies {equal = eq} x f) alphabet)
  fun stateTransitions (HoaState (p, cs, ts)) = concat (map (fn HoaTransition (f, q) => expandTransition p (mapFormula f) q) ts)
  val transitions = concat (map stateTransitions states)
  val accepting = map (fn HoaState (p, cs, ts) => p) (filter (fn HoaState (p, cs, ts) => not (null cs)) states)
  in (aps, Nbaei (alphabet, initial, transitions, accepting)) end
fun toHoaAutomaton aps (Nbaei (a, i, t, c)) = let
  val Set nodes = sup_seta {equal = eq}
    (image (fn (p, (_, q)) => insert {equal = eq} p (insert {equal = eq} q bot_set)) (Set t));
  val properties =
    [HoaVersion "v1"] @
    [HoaProperties ["trans-labels", "explicit-labels", "state-acc"]] @
    [HoaAtomicPropositions (nat_of_integer (length aps), aps)] @
    [HoaAcceptanceConditionName "Buchi"] @
    [HoaAcceptanceCondition "1 Inf(0)"] @
    map HoaStartState i @
    [HoaStateCount (nat_of_integer (length nodes))]
  fun literal ps k = if member {equal = eq} (nth (aps, k)) ps
    then Variable (nat_of_integer k) else Negation (Variable (nat_of_integer k))
  fun formula ps = foldl' True Conjunction (map (literal ps) (upto (length aps)))
  fun transitions p = map (fn (p, (a, q)) => HoaTransition (formula a, q)) (filter (fn (p', (a, q)) => p' = p) t)
  fun state p = HoaState (p, if member {equal = eq} p (Set c) then [nat_of_integer 0] else [], transitions p)
  val states = map state nodes
  in HoaAutomaton (properties, states) end

fun showNbaei f g (Nbaei (a, i, t, c)) =
  showList f a ^ "\n" ^
  showList g i ^ "\n" ^
  showList (showTuple g (showTuple f g)) t ^ "\n" ^
  showList g c ^ "\n"
fun write_automaton f path automaton = let
	fun t (p, (a, q)) = Int.toString (integer_of_nat p) ^ " " ^ f a ^ " " ^ Int.toString (integer_of_nat q) ^ "\n"
	val output = TextIO.openOut path
	fun write [] = () | write (x :: xs) = (TextIO.output (output, t x); write xs)
	val _ = write (transitionei automaton)
	val _ = TextIO.closeOut output
	in () end

val parameters = CommandLine.arguments ()
val _ = case hd parameters of
	"help" => println "Available Commands: help | complement <automaton> | equivalence <automaton1> <automaton2>" |
	"complement" => let
	  val (aps, nbaei) = toNbaei (parseHoaAutomaton (nth (parameters, 1)))
	  val nbai = nbae_nba_impl eq eq nbaei
	  val complement = toHoaAutomaton aps (complement_impl nbai)
	  in print (showHoaAutomaton complement) end |
	"complement_quick" => let
	  val (aps, nbaei) = toNbaei (parseHoaAutomaton (nth (parameters, 1)))
	  val nbai = nbae_nba_impl eq eq nbaei
	  val complement = complement_impl nbai
	  in write_automaton (showSet showString) (nth (parameters, 2)) complement end |
	"equivalence" => let
	  val (aps1, nbaei1) = toNbaei (parseHoaAutomaton (nth (parameters, 1)))
	  val (aps2, nbaei2) = toNbaei (parseHoaAutomaton (nth (parameters, 2)))
	  val nbai1 = nbae_nba_impl eq eq nbaei1
	  val nbai2 = nbae_nba_impl eq eq nbaei2
	  in println (Bool.toString (language_equal_impl {equal = eq} nbai1 nbai2)) end |
	"product" => let
	  val (aps1, nbaei1) = toNbaei (parseHoaAutomaton (nth (parameters, 1)))
	  val (aps2, nbaei2) = toNbaei (parseHoaAutomaton (nth (parameters, 2)))
	  val nbai1 = nbae_nba_impl eq eq nbaei1
	  val nbai2 = nbae_nba_impl eq eq nbaei2
	  val product = product_impl {equal = eq} nbai1 nbai2
	  in write_automaton (showSet showString) (nth (parameters, 3)) product end |
	"parse" => let
	  val ha = parseHoaAutomaton (nth (parameters, 1))
	  val (aps, nbaei) = toNbaei ha
	  val _ = println (showNbaei (showSet showString) showNat nbaei)
	  in print (showHoaAutomaton (toHoaAutomaton aps nbaei)) end