mealy-decompose/app/LStarMain.hs

module Main where

import DotParser
import LStar
import Mealy

import Control.Monad (when)
import Control.Monad.Trans.Class
import Control.Monad.Trans.State.Strict
import System.Environment
import System.IO
import Data.Maybe (mapMaybe)
import Text.Megaparsec

debugOutput :: Bool
debugOutput = False

semanticsForState :: MealyMachine s i o -> s -> [i] -> o
semanticsForState _ _ [] = error ""
semanticsForState MealyMachine{..} q [a] = fst (behaviour q a)
semanticsForState m@MealyMachine{..} q (a:w) = semanticsForState m (snd (behaviour q a)) w


main :: IO ()
main = do
  [dotFile] <- getArgs
  print dotFile
  transitions <- mapMaybe (parseMaybe parseTransFull) . lines <$> readFile dotFile

  let machine = convertToMealy transitions
      mq0 = semanticsForState machine (initialState machine)
      mq = countingMQ (\w -> when debugOutput (print w) >> return (mq0 w))

  let loop table = do
        lift $ putStrLn "Making the table closed and consistent"
        (table2, b) <- makeClosedAndConsistentA mq table
        let (_, size, _, _) = createHypothesis table2

        inp <- lift $ do
          putStrLn (if b then "Table changed" else "Table did not changed")
          putStrLn (show size <> " states")
          putStr "> "
          hFlush stdout
          getLine

        if inp == ""
          then return size
          else do
            let cex = read inp
            table3 <- processCounterexampleA cex mq table2
            loop table3

      learner = do
        table <- initialiseA (inputs machine) mq
        loop table

  (a, b) <- runStateT learner 0

  print a
  putStrLn $ "MQs: " <> show b