script to input-decompose a model

.gitignore

@@ -1,3 +1,3 @@
 dist-newstyle/
 cabal.project.local
-
+*.prof

app/Playground.hs

@@ -1,43 +1,120 @@
 module Main where
 
-import DotParser ( convertToMealy, parseTransFull )
-import Mealy ( MealyMachine(..) )
-import SplittingTree ( PRState(..), refine, initialPRState )
-import StateIdentifiers ( stateIdentifierFor )
-import Trie qualified as Trie
+import Bisimulation (bisimulation2, empty, equate, equivalent)
+import DotParser (convertToMealy, parseTransFull)
+import Mealy (MealyMachine (..), outputFunction, transitionFunction)
+import SplittingTree (PRState (..), initialPRState, refine)
+import StateIdentifiers (stateIdentifierFor)
+import Trie qualified
 
-import Control.Monad.Trans.State ( execStateT )
+import Control.Monad.Trans.State (execStateT)
+import Data.List qualified as List
 import Data.Map.Strict qualified as Map
-import Data.Maybe ( mapMaybe )
-import System.Environment ( getArgs )
-import Text.Megaparsec ( parseMaybe )
+import Data.Maybe (isJust, mapMaybe)
+import Data.Set qualified as Set
+import System.Environment (getArgs)
+import Text.Megaparsec (parseMaybe)
 
 main :: IO ()
 main = do
-  [dotFile] <- getArgs
-  print dotFile
-  transitions <- mapMaybe (parseMaybe parseTransFull) . lines <$> readFile dotFile
+  args <- getArgs
+  case args of
+    ("HSI" : ls) -> mainHSI ls
+    ("InputDecomp" : ls) -> mainInputDecomp ls
+    _ -> putStrLn "Please provide one of [HSI, InputDecomp]"
 
-  -- convert to mealy
-  let
-    MealyMachine{..} = convertToMealy transitions
-    outputFuns = [(i, fun) | i <- inputs, let fun s = fst (behaviour s i)]
-    reverseTransitionMaps i = Map.fromListWith (++) [ (t, [s]) | s <- states, let t = snd (behaviour s i)]
-    reverseFuns = [(i, fun) | i <- inputs, let m = reverseTransitionMaps i, let fun s = Map.findWithDefault [] s m]
+mainHSI :: [String] -> IO ()
+mainHSI args = case args of
+  [dotFile] -> run dotFile
+  _ -> putStrLn "Please provide a dot file"
+ where
+  run dotFile = do
+    print dotFile
+    transitions <- mapMaybe (parseMaybe parseTransFull) . lines <$> readFile dotFile
 
-  PRState{..} <- execStateT (refine print outputFuns reverseFuns) (initialPRState states)
+    -- convert to mealy
+    let
+      MealyMachine{..} = convertToMealy transitions
+      outputFuns = [(i, fun) | i <- inputs, let fun s = fst (behaviour s i)]
+      reverseTransitionMaps i = Map.fromListWith (++) [(t, [s]) | s <- states, let t = snd (behaviour s i)]
+      reverseFuns = [(i, fun) | i <- inputs, let m = reverseTransitionMaps i, let fun s = Map.findWithDefault [] s m]
 
-  putStrLn "\nPARTITION"
-  print partition
+    PRState{..} <- execStateT (refine print outputFuns reverseFuns) (initialPRState states)
 
-  putStrLn "\nTREE"
-  print splittingTree
+    putStrLn "\nPARTITION"
+    print partition
 
-  let
-    siFor s = stateIdentifierFor s partition splittingTree
+    putStrLn "\nTREE"
+    print splittingTree
 
-  putStrLn "\nHARMONISED STATE IDENTIFIERS"
-  sis <- mapM (\s -> let si = siFor s in print (Trie.toList si) >> return si) states
+    let
+      siFor s = stateIdentifierFor s partition splittingTree
 
-  putStrLn "\nW-SET"
-  print (Trie.toList . foldr Trie.union Trie.empty $ sis)
+    putStrLn "\nHARMONISED STATE IDENTIFIERS"
+    sis <- mapM (\s -> let si = siFor s in print (Trie.toList si) >> return si) states
+
+    putStrLn "\nW-SET"
+    print (Trie.toList . foldr Trie.union Trie.empty $ sis)
+
+-- Interleaving composition of restriction to subalphabets
+-- precondigiotn: alph1 and alph2 have no common elements
+interleavingComposition :: Ord i => [i] -> [i] -> MealyMachine s i o -> MealyMachine (s, s) i o
+interleavingComposition alph1 alph2 m =
+  MealyMachine
+    { states = error "states should not be necessary"
+    , inputs = alph1 ++ alph2
+    , outputs = error "outputs should not be necessary"
+    , behaviour = \(s1, s2) i ->
+        case Map.lookup i alphLookup of
+          Just False -> let (o, t) = behaviour m s1 i in (o, (t, s2))
+          Just True -> let (o, t) = behaviour m s2 i in (o, (s1, t))
+          Nothing -> error "symbol not in either alphabet"
+    , initialState = (initialState m, initialState m)
+    }
+ where
+  alphLookup = Map.fromList ([(a, False) | a <- alph1] ++ [(a, True) | a <- alph2])
+
+mainInputDecomp :: [String] -> IO ()
+mainInputDecomp args = case args of
+  [dotFile] -> run dotFile
+  _ -> putStrLn "Please provide a dot file"
+ where
+  run dotFile = do
+    print dotFile
+    transitions <- mapMaybe (parseMaybe parseTransFull) . lines <$> readFile dotFile
+
+    let model = convertToMealy transitions
+        composition i j = interleavingComposition [i] [j] model
+        bisim i j =
+          let compo = composition i j
+           in bisimulation2 [i, j]
+                (outputFunction model) (transitionFunction model) (initialState model)
+                (outputFunction compo) (transitionFunction compo) (initialState compo)
+        dependent i j = isJust $ bisim i j
+        dependentPairs = [(i, j) | i <- inputs model, j <- inputs model, j > i, dependent i j]
+
+    print $ length (states model)
+    print $ length (inputs model)
+    print $ length (outputs model)
+
+    putStrLn "Dependent pairs:"
+    print $ length dependentPairs
+
+    let dps = Set.fromList dependentPairs
+        dpsFun i j = i == j || (i, j) `Set.member` dps || (j, i) `Set.member` dps
+        trans =
+          null [(i, j, k) | i <- inputs model, j <- inputs model, dpsFun i j, k <- inputs model, dpsFun j k, not (dpsFun i k)]
+
+    putStrLn "Transitive?"
+    print trans
+
+    let closure = foldr (uncurry equate) empty dependentPairs
+        step [] = Nothing
+        step ls@(i : _) = Just (List.partition (\j -> equivalent i j closure) ls)
+        classes = List.unfoldr step (inputs model)
+
+    mapM_ print classes
+    case length classes of
+      0 -> putStrLn "ERROR"
+      1 -> putStrLn "INDECOMPOSABLE"
+      n -> putStrLn ("MAYBE DECOMPOSABLE: " ++ show n ++ " classes")

other/decompose_fsm_optimise.py

@@ -37,7 +37,7 @@ def main():
   print(f'Input FSM: {len(machine.states)} states, {len(machine.inputs)} inputs, and {len(machine.outputs)} outputs')
 
   if args.timeout != None:
-    def timeout_handler(signum, frame):
+    def timeout_handler(*_):
       with open(record_file, 'a') as file:
         last_two_comps = '/'.join(args.filename.split('/')[-2:])
         file.write(f'{last_two_comps}\t{len(machine.states)}\t{len(machine.inputs)}\t{len(machine.outputs)}\t{args.weak}\t{c}\tTIMEOUT\n')

src/Mealy.hs

@@ -8,6 +8,12 @@ data MealyMachine s i o = MealyMachine
   , initialState :: s
   }
 
+outputFunction :: MealyMachine s i o -> s -> i -> o
+outputFunction MealyMachine{..} s i = fst (behaviour s i)
+
+transitionFunction :: MealyMachine s i o -> s -> i -> s
+transitionFunction MealyMachine{..} s i = snd (behaviour s i)
+
 exampleMM :: MealyMachine String Char String
 exampleMM =
   let states = ["q0", "q1", "q2", "q3"]
@@ -21,5 +27,6 @@ exampleMM =
       behaviour "q2" 'b' = ("twee", "q0")
       behaviour "q1" 'b' = ("vier", "q3")
       behaviour "q3" 'b' = ("twee", "q1")
+      behaviour _ _ = error "undefined behaviour of exampleMM"
       initialState = "q0"
-  in MealyMachine {..}
+   in MealyMachine{..}