Commit 3b52e113 authored by Hans-Peter Deifel's avatar Hans-Peter Deifel 🐢

wta: Document and clean up code

parent 899c6cba
...@@ -307,6 +307,9 @@ executable random-wta ...@@ -307,6 +307,9 @@ executable random-wta
, megaparsec >= 7 && <8 , megaparsec >= 7 && <8
, scientific >= 0.3 && <0.4 , scientific >= 0.3 && <0.4
, containers >= 0.6 && <0.7 , containers >= 0.6 && <0.7
, prettyprinter >= 1.2.1
, prettyprinter-ansi-terminal >= 1.1.1.2
, prettyprinter-convert-ansi-wl-pprint
ghc-options: -Wall -Wno-name-shadowing ghc-options: -Wall -Wno-name-shadowing
test-suite random-wta-tests test-suite random-wta-tests
......
...@@ -2,6 +2,7 @@ ...@@ -2,6 +2,7 @@
{-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE LambdaCase #-} {-# LANGUAGE LambdaCase #-}
-- | Genator for random weighted tree automata.
module Generator module Generator
( genWTA ( genWTA
, runGenerator , runGenerator
...@@ -29,23 +30,35 @@ import Probability ...@@ -29,23 +30,35 @@ import Probability
import IndexedTransition ( IndexedTransition ) import IndexedTransition ( IndexedTransition )
import qualified IndexedTransition import qualified IndexedTransition
data EdgeConfig = ZeroFrequency Probability | NumTransitions Int
-- | Decides how many non-zero transitions are generated.
data EdgeConfig
-- | Generate zero transitions with a given probability.
= ZeroFrequency Probability
-- | Generate a fixed number of non-zero transitions.
| NumTransitions Int
-- Configuration for the automaton generator.
data GeneratorConfig m = GeneratorConfig data GeneratorConfig m = GeneratorConfig
{ spec :: WTASpec m { spec :: WTASpec m -- ^ The automaton to generate.
, zeroPolicy :: EdgeConfig , zeroPolicy :: EdgeConfig -- ^ How many edges to generate.
, differentValues :: Maybe Int , differentValues :: Maybe Int -- ^ How many different monoid values to generate.
} }
type Generator m = ReaderT (GeneratorConfig m) IO type Generator m = ReaderT (GeneratorConfig m) IO
zeroFreq :: GeneratorConfig m -> Probability
zeroFreq GeneratorConfig { zeroPolicy = ZeroFrequency p } = p
zeroFreq _ = error "zeroFreq: unexpected out degree" -- TODO Ugly as hell
-- | Acutally run the generator with the given config.
runGenerator :: GeneratorConfig m -> Generator m a -> IO a runGenerator :: GeneratorConfig m -> Generator m a -> IO a
runGenerator config action = runReaderT action config runGenerator config action = runReaderT action config
zeroFreq :: GeneratorConfig m -> Probability
zeroFreq GeneratorConfig { zeroPolicy = ZeroFrequency p } = p
zeroFreq _ = error "zeroFreq: unexpected out degree" -- Ugly as hell
genMonoidValue :: Generator m m genMonoidValue :: Generator m m
genMonoidValue = asks ((monoid . spec) &&& differentValues) >>= \case genMonoidValue = asks ((monoid . spec) &&& differentValues) >>= \case
(Powerset, Nothing) -> liftIO randomIO (Powerset, Nothing) -> liftIO randomIO
...@@ -104,7 +117,6 @@ genTransitionsZeroFreq = do ...@@ -104,7 +117,6 @@ genTransitionsZeroFreq = do
n <- asks (numStates . spec) n <- asks (numStates . spec)
V.replicateM n genStateTransitions V.replicateM n genStateTransitions
-- TODO Implement (Random IndexedTransition)
uniqueTransitions :: Int -> IndexedTransition -> IO [IndexedTransition] uniqueTransitions :: Int -> IndexedTransition -> IO [IndexedTransition]
uniqueTransitions num idxMax@(IndexedTransition.Index max) uniqueTransitions num idxMax@(IndexedTransition.Index max)
| fromIntegral num < fromIntegral max * ((7 :: Integer) % 10) = uniqueTransitionsByGeneration | fromIntegral num < fromIntegral max * ((7 :: Integer) % 10) = uniqueTransitionsByGeneration
...@@ -114,22 +126,22 @@ uniqueTransitions num idxMax@(IndexedTransition.Index max) ...@@ -114,22 +126,22 @@ uniqueTransitions num idxMax@(IndexedTransition.Index max)
uniqueTransitionsByGeneration uniqueTransitionsByGeneration
:: Int -> IndexedTransition -> IO [IndexedTransition] :: Int -> IndexedTransition -> IO [IndexedTransition]
uniqueTransitionsByGeneration num (IndexedTransition.Index max) = helper uniqueTransitionsByGeneration num max = helper
S.empty S.empty
num num
where where
helper m 0 = return $ coerce (S.toList m) helper m 0 = return $ S.toList m
helper m c = do helper m c = do
x <- randomRIO (0, max - 1) x <- randomRIO (0, max - 1)
if x `S.member` m then helper m c else helper (S.insert x m) (c - 1) if x `S.member` m then helper m c else helper (S.insert x m) (c - 1)
uniqueTransitionsByElimination uniqueTransitionsByElimination
:: Int -> IndexedTransition -> IO [IndexedTransition] :: Int -> IndexedTransition -> IO [IndexedTransition]
uniqueTransitionsByElimination num (IndexedTransition.Index max) = helper uniqueTransitionsByElimination num max = helper
whole whole
num num
where where
helper free 0 = return $ coerce (S.toList (S.difference whole free)) helper free 0 = return $ S.toList (S.difference whole free)
helper free c = do helper free c = do
idx <- randomRIO (0, S.size free - 1) idx <- randomRIO (0, S.size free - 1)
let x = S.elemAt idx free let x = S.elemAt idx free
...@@ -145,7 +157,7 @@ genTransitionsNumTrans numTransitions = do ...@@ -145,7 +157,7 @@ genTransitionsNumTrans numTransitions = do
numTransitions' <- if fromIntegral numTransitions > maxT numTransitions' <- if fromIntegral numTransitions > maxT
then do then do
let cap = IndexedTransition.fromIndexd maxT let cap = IndexedTransition.fromIndexdTransition maxT
lift $ hPutStrLn lift $ hPutStrLn
stderr stderr
( "warning: More transitions than possible requested. Capping at " ( "warning: More transitions than possible requested. Capping at "
......
{-# LANGUAGE GADTs #-} {-# LANGUAGE GADTs #-}
{-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE OverloadedStrings #-}
-- | Generator for the input format of the implementation of WTA bisimulation at
-- https://people.cs.umu.se/~johanna/bisimulation/
--
-- Note that to the best of my knowledge, only supports the powerset functor
-- with weights that are textually hardcoded as 1.0.
module Hoegberg (hoegbergWTA) where module Hoegberg (hoegbergWTA) where
import qualified Data.Vector as V import qualified Data.Vector as V
...@@ -42,6 +47,8 @@ accepting wta = ...@@ -42,6 +47,8 @@ accepting wta =
accepting1 :: Int -> Builder accepting1 :: Int -> Builder
accepting1 s = Build.decimal s <> " 1.0\n" accepting1 s = Build.decimal s <> " 1.0\n"
-- | Print a WTA. See the module level documentation for why this only accepts
-- "Bool" as monoid.
hoegbergWTA :: WTA Bool -> Builder hoegbergWTA :: WTA Bool -> Builder
hoegbergWTA wta = hoegbergWTA wta =
declareState (spec wta) <> "\n" <> rules wta <> "%%%\n" <> accepting wta declareState (spec wta) <> "\n" <> rules wta <> "%%%\n" <> accepting wta
...@@ -2,25 +2,53 @@ ...@@ -2,25 +2,53 @@
{-# LANGUAGE DerivingStrategies #-} {-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-}
module IndexedTransition (IndexedTransition(..), maxIndex, fromIndex, index) where -- | A bijection from transitions to integers.
--
-- This module provides functions to convert transitions to and from continuous
-- integer indices without loss of information (for a given WTA).
--
-- In particular, this allows for easy enumeration of all transitions and
-- enables choosing a small set of transitions from a potentially very large set
-- of /all/ possible transitions for a given WTA.
--
-- Transitions are ordered by
--
-- 1. Source state
-- 2. Arity
-- 3. Symbol with that arity
-- 4. Successor states in lexicographic order
--
-- Transition indices are then simply the indices into the list of all
-- transitions for the given WTA, ordered by the above criteria.
module IndexedTransition
( IndexedTransition(..)
, maxIndex
, fromIndex
, index
)
where
import Data.Vector ( Vector ) import Data.Vector ( Vector )
import qualified Data.Vector as V import qualified Data.Vector as V
import Data.Maybe import Data.Maybe
import Data.Tuple import Data.Tuple
import System.Random
import Types import Types
newtype IndexedTransition = Index { fromIndexd :: Integer } -- | Index into the set of all transitions for a given WTA
deriving newtype (Num, Eq, Ord) newtype IndexedTransition = Index { fromIndexdTransition :: Integer }
deriving newtype (Num, Eq, Ord, Random, Enum)
deriving (Show) deriving (Show)
-- | Return __one more than__ the maximum transition index for a given WTA.
maxIndex :: WTASpec m -> IndexedTransition maxIndex :: WTASpec m -> IndexedTransition
maxIndex spec = maxIndex spec =
let n = numStates spec let n = numStates spec
(t, _) = transitionsPerState spec (t, _) = transitionsPerState spec
in Index (fromIntegral n * t) in Index (fromIntegral n * t)
-- | Convert the given index to its corresponding transition.
fromIndex :: WTASpec m -> IndexedTransition -> (State, Transition ()) fromIndex :: WTASpec m -> IndexedTransition -> (State, Transition ())
fromIndex spec (Index i) = fromIndex spec (Index i) =
let n = numStates spec let n = numStates spec
...@@ -49,6 +77,7 @@ fromIndex spec (Index i) = ...@@ -49,6 +77,7 @@ fromIndex spec (Index i) =
} }
in (State (fromIntegral state), trans) in (State (fromIntegral state), trans)
-- | Convert the given transition to its corresponding index.
index :: WTASpec m1 -> State -> Transition m2 -> IndexedTransition index :: WTASpec m1 -> State -> Transition m2 -> IndexedTransition
index spec (State state) trans = index spec (State state) trans =
let (t, symbolSums) = transitionsPerState spec let (t, symbolSums) = transitionsPerState spec
...@@ -65,14 +94,25 @@ index spec (State state) trans = ...@@ -65,14 +94,25 @@ index spec (State state) trans =
-- Helpers -- Helpers
-- | Convert a given summand number to its arity
summandArity :: WTASpec m -> Int -> Int summandArity :: WTASpec m -> Int -> Int
summandArity spec summand = V.findIndices (/= 0) (numSymbols spec) V.! summand summandArity spec summand = V.findIndices (/= 0) (numSymbols spec) V.! summand
-- | Convert a given arity to its summand index
aritySummand :: WTASpec m -> Int -> Int aritySummand :: WTASpec m -> Int -> Int
aritySummand spec arity = aritySummand spec arity =
let arities = numSymbols spec let arities = numSymbols spec
in V.length (V.filter (/= 0) (V.take arity arities)) in V.length (V.filter (/= 0) (V.take arity arities))
-- | Return the maximum number of transitions per state for this WTA as well as
-- a vector that contains at index @i@ the maximum number of transitions per
-- state with arity @i@ or less.
--
-- Therefore,
--
-- @
-- fst (transitionsPerState w) == last (snd (transitionsPerState w))
-- @
transitionsPerState :: WTASpec m -> (Integer, Vector Integer) transitionsPerState :: WTASpec m -> (Integer, Vector Integer)
transitionsPerState spec = transitionsPerState spec =
let n :: Integer = fromIntegral $ numStates spec let n :: Integer = fromIntegral $ numStates spec
......
...@@ -19,6 +19,10 @@ import Numeric ...@@ -19,6 +19,10 @@ import Numeric
import System.IO import System.IO
import System.Exit import System.Exit
import Control.Applicative import Control.Applicative
import Data.Text.Prettyprint.Doc
import Data.Text.Prettyprint.Doc.Util
import Data.Text.Prettyprint.Doc.Render.Terminal
import Data.Text.Prettyprint.Convert.AnsiWlPprint
import Types import Types
import Generator import Generator
...@@ -91,9 +95,12 @@ parseOpts = ...@@ -91,9 +95,12 @@ parseOpts =
( Options.long "symbols" ( Options.long "symbols"
<> Options.metavar "NUM,NUM,..." <> Options.metavar "NUM,NUM,..."
<> Options.help <> Options.help
"Comma separated list of symbols per arity. E.g. 2,0,1 means two symbols with arity 0, non with arity 1 and one with arity two" ( "Comma separated list of symbols per arity."
<> " E.g. 2,0,1 means two symbols with arity 0,"
<> "non with arity 1 and one with arity two"
)
) )
<*> parseZeroFreq <*> parseEdgeConfig
<*> Options.optional <*> Options.optional
(Options.option Options.auto (Options.long "random-state")) (Options.option Options.auto (Options.long "random-state"))
<*> Options.optional <*> Options.optional
...@@ -102,13 +109,20 @@ parseOpts = ...@@ -102,13 +109,20 @@ parseOpts =
( Options.long "different-values" ( Options.long "different-values"
<> Options.metavar "NUM" <> Options.metavar "NUM"
<> Options.help <> Options.help
"Maximal number of differnt monoid values to generate" ("Maximal number of differnt monoid values to generate."
<> "This is useful to limit the number of blocks in the initial partition."
)
)
)
<*> Options.switch
(Options.long "hoegberg" <> Options.help
("Generate output in format suiteable for Johanna Högbergs Java implementation."
<> " See https://people.cs.umu.se/~johanna/bisimulation/"
) )
) )
<*> Options.switch (Options.long "hoegberg" <> Options.help "Generate output in format suiteable for Hoegbergs Java implementation.")
parseZeroFreq :: Options.Parser EdgeConfig parseEdgeConfig :: Options.Parser EdgeConfig
parseZeroFreq = parseEdgeConfig =
(ZeroFrequency <$> Options.option (ZeroFrequency <$> Options.option
(Options.eitherReader readProbability) (Options.eitherReader readProbability)
( Options.long "zero-frequency" ( Options.long "zero-frequency"
...@@ -122,7 +136,9 @@ parseZeroFreq = ...@@ -122,7 +136,9 @@ parseZeroFreq =
<|> (NumTransitions <$> Options.option <|> (NumTransitions <$> Options.option
Options.auto Options.auto
(Options.long "transitions" <> Options.metavar "NUM" <> Options.help (Options.long "transitions" <> Options.metavar "NUM" <> Options.help
"Number of transitions to generate. They will be distributed randomly over states." ( "Number of transitions to generate."
<> "They will be distributed randomly over states."
)
) )
) )
...@@ -133,10 +149,34 @@ withSpec opts f = case optMonoid opts of ...@@ -133,10 +149,34 @@ withSpec opts f = case optMonoid opts of
, numSymbols = optSymbols opts , numSymbols = optSymbols opts
} }
example :: Doc AnsiStyle
example =
"Example:"
<> line
<> line
<> " random-wta --monoid Z,max --states 3 --symbols 1,2,3"
<> line
<> line
<> reflow "This generates a WTA with three states for the functor"
<> softline
<> "Z×X^(1 + 2×X + 3×X^2)"
<> softline
<> reflow "with roughly 30% of all possible edges, chosen at random."
<> softline
<> reflow "To control the number of edges, use --zero-frequency"
<> softline
<> reflow "or --transitions."
main :: IO () main :: IO ()
main = do main = do
let optSpec = let optSpec = Options.info
Options.info (parseOpts Options.<**> Options.helper) Options.fullDesc (parseOpts Options.<**> Options.helper)
( Options.fullDesc
<> Options.header "Generator for random weighted tree automata"
<> Options.footerDoc (Just (toAnsiWlPprint example))
)
opts <- Options.execParser optSpec opts <- Options.execParser optSpec
case optMonoid opts of case optMonoid opts of
...@@ -154,5 +194,8 @@ main = do ...@@ -154,5 +194,8 @@ main = do
genWTA genWTA
putStrLn $ "# Random state for this automaton: '" <> show randGen <> "'" putStrLn $ "# Random state for this automaton: '" <> show randGen <> "'"
case monoid spec of case monoid spec of
Powerset | optHoegberg opts -> T.putStr (Build.toLazyText (hoegbergWTA wta)) Powerset | optHoegberg opts ->
T.putStr (Build.toLazyText (hoegbergWTA wta))
_ | optHoegberg opts ->
hPutStrLn stderr "error: Hoegberg output only supports powerset"
_ -> T.putStr (Build.toLazyText (buildWTA wta)) _ -> T.putStr (Build.toLazyText (buildWTA wta))
{-# LANGUAGE GADTs #-} {-# LANGUAGE GADTs #-}
-- | Printer for CoPaR's input format, i.e. coalgebra specifications.
module Output (buildWTA) where module Output (buildWTA) where
import qualified Data.Vector as V import qualified Data.Vector as V
...@@ -89,6 +90,8 @@ buildStates wta = foldMap ...@@ -89,6 +90,8 @@ buildStates wta = foldMap
(V.zip3 (V.fromList indices) (stateValue wta) (stateTransitions wta)) (V.zip3 (V.fromList indices) (stateValue wta) (stateTransitions wta))
where indices = [0 .. V.length (stateValue wta) - 1] where indices = [0 .. V.length (stateValue wta) - 1]
-- | Print a WTA as coalgebra specification suitable for CoPaR.
buildWTA :: WTA m -> Builder buildWTA :: WTA m -> Builder
buildWTA a = wtaFunctor (spec a) <> "\n" <> buildStates a buildWTA a = wtaFunctor (spec a) <> "\n" <> buildStates a
......
{-# LANGUAGE DerivingStrategies #-} {-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-}
module Probability -- | Arbitrary precision floating point numbers between [0,1] that can be used
( Probability(..) -- as a probability value.
, readProbability module Probability (Probability(..), readProbability, decide) where
, decide
, fromRationalApprox
)
where
import System.Random import System.Random
import Data.Scientific import Data.Scientific
-- | Arbitrary precision floating point numbers between [0,1] that can be used
-- as a probability value.
newtype Probability = Probability Scientific newtype Probability = Probability Scientific
deriving newtype (Show,Fractional,Num) deriving newtype (Show,Fractional,Num)
-- | Read an arbitrary precision floating point number from a string. Valid
-- formats are:
--
-- - 0
-- - 1
-- - 1.0
-- - 0.[0..9]*
--
-- which means that leading zeros are not allowed. in particular, @00@, @1.@ and
-- similar verboten for simplicity.
readProbability :: String -> Either String Probability readProbability :: String -> Either String Probability
readProbability input = Probability <$> case input of readProbability input = Probability <$> case input of
"0" -> Right (scientific 0 0) "0" -> Right (scientific 0 0)
...@@ -27,22 +37,13 @@ readProbability input = Probability <$> case input of ...@@ -27,22 +37,13 @@ readProbability input = Probability <$> case input of
_ -> failure _ -> failure
where failure = Left "Could not parse probability" where failure = Left "Could not parse probability"
-- | Return 'True' randomly with the given probability and 'False' otherwise.
--
-- Uses the global random number generator.
decide :: Probability -> IO Bool decide :: Probability -> IO Bool
decide (Probability science) = do decide (Probability science) = do
let digits = coefficient science let digits = coefficient science
let exp = negate (base10Exponent science) let exp = negate (base10Exponent science)
randomNumber <- randomRIO (0, (10 ^ exp) - 1) randomNumber <- randomRIO (0, (10 ^ exp) - 1)
return $ randomNumber < digits return $ randomNumber < digits
fromRationalApprox :: Rational -> Probability
fromRationalApprox r =
Probability $ clamp 0 1 $ case fromRationalRepetend (Just 100) r of
Left (s, _) -> s
-- TODO Maybe make this case more precise. Currently, 1/3 gets converted to
-- 0.3, which might not be precise enough.
Right (s, _) -> s
clamp :: (Ord a, Num a) => a -> a -> a -> a
clamp low high x | x < low = low
| x > high = high
| otherwise = x
...@@ -6,7 +6,7 @@ import Test.Hspec ...@@ -6,7 +6,7 @@ import Test.Hspec
import Test.QuickCheck import Test.QuickCheck
import qualified Data.Vector as V import qualified Data.Vector as V
import Data.List (nub) import Data.List ( nub )
import Types import Types
import qualified IndexedTransition import qualified IndexedTransition
...@@ -32,7 +32,7 @@ main = hspec $ do ...@@ -32,7 +32,7 @@ main = hspec $ do
describe "maxIndex" $ do describe "maxIndex" $ do
it "doesn't overflow for large values" $ do it "doesn't overflow for large values" $ do
let wta = WTASpec MaxInt 72000 (V.fromList [0, 0, 0, 0, 4]) let wta = WTASpec MaxInt 72000 (V.fromList [0, 0, 0, 0, 4])
IndexedTransition.maxIndex wta `shouldSatisfy` (>0) IndexedTransition.maxIndex wta `shouldSatisfy` (> 0)
describe "Generator" $ describe "uniqueTransitions" $ do describe "Generator" $ describe "uniqueTransitions" $ do
it "generates unique transitions" $ do it "generates unique transitions" $ do
...@@ -54,7 +54,7 @@ main = hspec $ do ...@@ -54,7 +54,7 @@ main = hspec $ do
it "doesn't generate a transition greater than max" $ do it "doesn't generate a transition greater than max" $ do
res <- maximum <$> uniqueTransitions 100 (IndexedTransition.Index 150) res <- maximum <$> uniqueTransitions 100 (IndexedTransition.Index 150)
res `shouldSatisfy` (<150) res `shouldSatisfy` (< 150)
instance Arbitrary IndexedTransition.IndexedTransition where instance Arbitrary IndexedTransition.IndexedTransition where
......
...@@ -17,38 +17,55 @@ where ...@@ -17,38 +17,55 @@ where
import Data.Vector ( Vector ) import Data.Vector ( Vector )
-- Powerset is not the monoid, it's ({True,False}, or)^X -- | Supported monoids
--
-- Note that powerset is not really the monoid, it's ({True,False}, or)^X
data MonoidType m where data MonoidType m where
MaxInt ::MonoidType Int MaxInt :: MonoidType Int
OrWord ::MonoidType Word OrWord :: MonoidType Word
Powerset ::MonoidType Bool Powerset :: MonoidType Bool
deriving instance Show (MonoidType m) deriving instance Show (MonoidType m)
-- | For each arity, the number of symbols -- | For each arity, the number of symbols
type SymbolSpec = Vector Int type SymbolSpec = Vector Int
-- | Type and size of an automaton.
data WTASpec m = WTASpec data WTASpec m = WTASpec
{ monoid :: MonoidType m { monoid :: MonoidType m
-- | Number of states
, numStates :: Int , numStates :: Int
-- | Number of symbols per arity
, numSymbols :: SymbolSpec , numSymbols :: SymbolSpec
} }
deriving instance Show m => Show (WTASpec m) deriving instance Show m => Show (WTASpec m)
-- | A state in the automaton
newtype State = State { fromState :: Int} newtype State = State { fromState :: Int}
deriving (Num,Show,Eq,Integral,Enum,Real,Ord) deriving (Num,Show,Eq,Integral,Enum,Real,Ord)
-- | A transition in the automaton. Note that the source state is not part of
-- this record, since it is implicit in the arry 'stateTransitions' of the 'WTA'
-- type.
data Transition m = Transition data Transition m = Transition