mirror of
https://github.com/Jaxan/nominal-lstar.git
synced 2025-04-27 14:47:45 +02:00
Cleaned up the cabal file and moved some bits around
This commit is contained in:
parent
d6173c4381
commit
16b0f6ed79
8 changed files with 80 additions and 74 deletions
|
@ -1,69 +0,0 @@
|
||||||
name: NominalAngluin
|
|
||||||
version: 0.1.0.0
|
|
||||||
license: UnspecifiedLicense
|
|
||||||
author: Joshua Moerman
|
|
||||||
copyright: (c) 2016 - 2020, Joshua Moerman
|
|
||||||
build-type: Simple
|
|
||||||
cabal-version: >=1.10
|
|
||||||
|
|
||||||
executable NominalAngluin
|
|
||||||
main-is: Main.hs
|
|
||||||
other-modules:
|
|
||||||
AbstractLStar,
|
|
||||||
Angluin,
|
|
||||||
Bollig,
|
|
||||||
Examples,
|
|
||||||
Examples.Contrived,
|
|
||||||
Examples.ContrivedNFAs,
|
|
||||||
Examples.Fifo,
|
|
||||||
Examples.NonResidual,
|
|
||||||
Examples.Residual,
|
|
||||||
Examples.RunningExample,
|
|
||||||
Examples.Stack,
|
|
||||||
NLStar,
|
|
||||||
ObservationTable,
|
|
||||||
Teacher,
|
|
||||||
Teachers.Teacher,
|
|
||||||
Teachers.Terminal,
|
|
||||||
Teachers.Whitebox
|
|
||||||
build-depends:
|
|
||||||
base >= 4.8 && < 5,
|
|
||||||
containers,
|
|
||||||
haskeline,
|
|
||||||
mtl,
|
|
||||||
NLambda >= 1.1
|
|
||||||
hs-source-dirs: src
|
|
||||||
default-language: Haskell2010
|
|
||||||
ghc-options: -O2 -Wall
|
|
||||||
|
|
||||||
executable NominalAngluin2
|
|
||||||
ghc-options:
|
|
||||||
-O2
|
|
||||||
main-is: Main2.hs
|
|
||||||
other-modules:
|
|
||||||
AbstractLStar,
|
|
||||||
Angluin,
|
|
||||||
Bollig,
|
|
||||||
Examples,
|
|
||||||
Examples.Contrived,
|
|
||||||
Examples.ContrivedNFAs,
|
|
||||||
Examples.Fifo,
|
|
||||||
Examples.NonResidual,
|
|
||||||
Examples.Residual,
|
|
||||||
Examples.RunningExample,
|
|
||||||
Examples.Stack,
|
|
||||||
NLStar,
|
|
||||||
ObservationTable,
|
|
||||||
Teacher,
|
|
||||||
Teachers.Teacher,
|
|
||||||
Teachers.Terminal,
|
|
||||||
Teachers.Whitebox
|
|
||||||
build-depends:
|
|
||||||
base >= 4.8 && < 5,
|
|
||||||
containers,
|
|
||||||
haskeline,
|
|
||||||
mtl,
|
|
||||||
NLambda >= 1.1
|
|
||||||
hs-source-dirs: src
|
|
||||||
default-language: Haskell2010
|
|
||||||
ghc-options: -O2 -Wall
|
|
|
@ -45,7 +45,7 @@ mainExample learnerName teacherName autName = do
|
||||||
let h = case read learnerName of
|
let h = case read learnerName of
|
||||||
NomLStar -> learnAngluinRows teacher
|
NomLStar -> learnAngluinRows teacher
|
||||||
NomLStarCol -> learnAngluin teacher
|
NomLStarCol -> learnAngluin teacher
|
||||||
NomNLStar -> learnBollig 1 1 teacher
|
NomNLStar -> learnBollig 0 0 teacher
|
||||||
print h
|
print h
|
||||||
|
|
||||||
mainWithIO :: String -> IO ()
|
mainWithIO :: String -> IO ()
|
14
bench/Bench.hs
Normal file
14
bench/Bench.hs
Normal file
|
@ -0,0 +1,14 @@
|
||||||
|
import Bollig
|
||||||
|
import Examples
|
||||||
|
import Teacher
|
||||||
|
|
||||||
|
import Criterion.Main
|
||||||
|
|
||||||
|
main :: IO ()
|
||||||
|
main = defaultMain [
|
||||||
|
bgroup "NomNLStar"
|
||||||
|
[ bench "NFA1 -" $ whnf (learnBollig 0 0) (teacherWithTargetNonDet 2 Examples.exampleNFA1)
|
||||||
|
, bench "NFA2 1" $ whnf (learnBollig 0 0) (teacherWithTargetNonDet 3 (Examples.exampleNFA2 1))
|
||||||
|
, bench "NFA2 2" $ whnf (learnBollig 0 0) (teacherWithTargetNonDet 4 (Examples.exampleNFA2 2))
|
||||||
|
]
|
||||||
|
]
|
62
nominal-lstar.cabal
Normal file
62
nominal-lstar.cabal
Normal file
|
@ -0,0 +1,62 @@
|
||||||
|
cabal-version: 2.2
|
||||||
|
name: nominal-lstar
|
||||||
|
version: 0.1.0.0
|
||||||
|
author: Joshua Moerman
|
||||||
|
copyright: (c) 2016 - 2020, Joshua Moerman
|
||||||
|
build-type: Simple
|
||||||
|
extra-source-files: README.md
|
||||||
|
|
||||||
|
common stuff
|
||||||
|
default-language: Haskell2010
|
||||||
|
ghc-options: -O2 -Wall
|
||||||
|
build-depends:
|
||||||
|
base >= 4.8 && < 5,
|
||||||
|
containers,
|
||||||
|
haskeline,
|
||||||
|
mtl,
|
||||||
|
NLambda >= 1.1
|
||||||
|
|
||||||
|
library
|
||||||
|
import: stuff
|
||||||
|
hs-source-dirs: src
|
||||||
|
exposed-modules:
|
||||||
|
AbstractLStar,
|
||||||
|
Angluin,
|
||||||
|
Bollig,
|
||||||
|
Examples,
|
||||||
|
Examples.Contrived,
|
||||||
|
Examples.ContrivedNFAs,
|
||||||
|
Examples.Fifo,
|
||||||
|
Examples.NonResidual,
|
||||||
|
Examples.Residual,
|
||||||
|
Examples.RunningExample,
|
||||||
|
Examples.Stack,
|
||||||
|
NLStar,
|
||||||
|
ObservationTable,
|
||||||
|
Teacher,
|
||||||
|
Teachers.Teacher,
|
||||||
|
Teachers.Terminal,
|
||||||
|
Teachers.Whitebox
|
||||||
|
|
||||||
|
executable NominalAngluin
|
||||||
|
import: stuff
|
||||||
|
hs-source-dirs: app
|
||||||
|
main-is: Main.hs
|
||||||
|
build-depends:
|
||||||
|
nominal-lstar
|
||||||
|
|
||||||
|
executable NominalAngluin2
|
||||||
|
import: stuff
|
||||||
|
hs-source-dirs: app
|
||||||
|
main-is: Main2.hs
|
||||||
|
build-depends:
|
||||||
|
nominal-lstar
|
||||||
|
|
||||||
|
benchmark bench
|
||||||
|
import: stuff
|
||||||
|
hs-source-dirs: bench
|
||||||
|
type: exitcode-stdio-1.0
|
||||||
|
main-is: Bench.hs
|
||||||
|
build-depends:
|
||||||
|
criterion,
|
||||||
|
nominal-lstar
|
|
@ -8,7 +8,7 @@ import Teacher
|
||||||
|
|
||||||
import Debug.Trace
|
import Debug.Trace
|
||||||
import NLambda
|
import NLambda
|
||||||
import Prelude (Bool (..), Int, Maybe (..), fst, snd, ($), (++), (.))
|
import Prelude (Bool (..), Int, Maybe (..), fst, snd, ($), (++), (.), (<=))
|
||||||
import qualified Prelude hiding ()
|
import qualified Prelude hiding ()
|
||||||
|
|
||||||
rowUnion :: NominalType i => Set (BRow i) -> BRow i
|
rowUnion :: NominalType i => Set (BRow i) -> BRow i
|
||||||
|
@ -20,8 +20,7 @@ rowUnion set = Prelude.uncurry union . setTrueFalse . partition snd $ map (\is -
|
||||||
setSecond a (x, _) = (x, a)
|
setSecond a (x, _) = (x, a)
|
||||||
|
|
||||||
boolImplies :: Bool -> Bool -> Bool
|
boolImplies :: Bool -> Bool -> Bool
|
||||||
boolImplies True False = False
|
boolImplies = (<=)
|
||||||
boolImplies _ _ = True
|
|
||||||
|
|
||||||
sublang :: NominalType i => BRow i -> BRow i -> Formula
|
sublang :: NominalType i => BRow i -> BRow i -> Formula
|
||||||
sublang r1 r2 = forAll fromBool $ pairsWithFilter (\(i1, f1) (i2, f2) -> maybeIf (i1 `eq` i2) (f1 `boolImplies` f2)) r1 r2
|
sublang r1 r2 = forAll fromBool $ pairsWithFilter (\(i1, f1) (i2, f2) -> maybeIf (i1 `eq` i2) (f1 `boolImplies` f2)) r1 r2
|
||||||
|
|
|
@ -57,4 +57,3 @@ exampleNFA2 n = automaton
|
||||||
`union` sum (fromList [map (Count i, , Count (i+1)) atoms | i <- [0 .. n-1]]))
|
`union` sum (fromList [map (Count i, , Count (i+1)) atoms | i <- [0 .. n-1]]))
|
||||||
(singleton Initial2)
|
(singleton Initial2)
|
||||||
(singleton (Count n))
|
(singleton (Count n))
|
||||||
|
|
||||||
|
|
|
@ -15,6 +15,7 @@ import qualified Prelude ()
|
||||||
data Res1 a = QR1 a | QR2 | QAncStar
|
data Res1 a = QR1 a | QR2 | QAncStar
|
||||||
deriving (Eq, Ord, Show, Generic, NominalType, Contextual)
|
deriving (Eq, Ord, Show, Generic, NominalType, Contextual)
|
||||||
|
|
||||||
|
-- Language L = { w a | a fresh for w }, but anchored with a new symbol
|
||||||
exampleResidual1 :: Automaton (Res1 Atom) DataInput
|
exampleResidual1 :: Automaton (Res1 Atom) DataInput
|
||||||
exampleResidual1 = automaton
|
exampleResidual1 = automaton
|
||||||
-- state space
|
-- state space
|
||||||
|
|
Loading…
Add table
Reference in a new issue