diff --git a/app/LStarMain.hs b/app/LStarMain.hs new file mode 100644 index 0000000..67cb09e --- /dev/null +++ b/app/LStarMain.hs @@ -0,0 +1,60 @@ +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 diff --git a/mealy-decompose.cabal b/mealy-decompose.cabal index 0d0b5ce..80056ee 100644 --- a/mealy-decompose.cabal +++ b/mealy-decompose.cabal @@ -46,6 +46,13 @@ executable mealy-decompose build-depends: mealy-decompose +executable mealy-decompose-lstar + import: stuff + hs-source-dirs: app + main-is: LStarMain.hs + build-depends: + mealy-decompose + executable mealy-decompose-playground import: stuff hs-source-dirs: app