Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Implement custom parser #31

Merged
merged 27 commits into from
Mar 21, 2024
Merged
Changes from 1 commit
Commits
Show all changes
27 commits
Select commit Hold shift + click to select a range
c9e6d39
[WIP] implement custom dsl
bsuehling Mar 9, 2024
6cf127f
implement formula parser
bsuehling Mar 9, 2024
6c583f7
fix some bugs
bsuehling Mar 10, 2024
29c6a76
feat: parse all .pg files in dir and sub-dirs
bsuehling Mar 12, 2024
513556b
feat: allow for error graphs
bsuehling Mar 12, 2024
afb9ab5
[WIP] implement json transformation
bsuehling Mar 12, 2024
982dcad
feat: implement LTL and CTL parser
bsuehling Mar 16, 2024
0e81a2f
feat: add hazards
bsuehling Mar 16, 2024
ff0f132
feat: add specifications
bsuehling Mar 16, 2024
084556a
feat: add initializations to json
bsuehling Mar 16, 2024
6b24e7d
Merge branch 'master' into feat/pg-dsl
bsuehling Mar 16, 2024
5f3f4d6
fix a bug in formula parsers
bsuehling Mar 16, 2024
1a27759
fix order of subformulas
bsuehling Mar 16, 2024
5b31551
conform to new json scheme
bsuehling Mar 16, 2024
5d368f1
fix more bugs
bsuehling Mar 16, 2024
89d8899
feat: implement type checking
bsuehling Mar 17, 2024
bc20a2f
feat: implement simple range checks
bsuehling Mar 18, 2024
a6a2364
feat: implement automatic precons
bsuehling Mar 18, 2024
69348f2
Merge branch 'master' into feat/pg-dsl
bsuehling Mar 18, 2024
ea7b9ad
fix bugs in json encoder
bsuehling Mar 18, 2024
0c61d97
Merge branch 'master' into feat/pg-dsl
bsuehling Mar 19, 2024
d0c85ae
fix: specifications use tl, not pl
bsuehling Mar 19, 2024
b1f2ba6
feat: add nofaults keyword
bsuehling Mar 20, 2024
0485c27
Merge branch 'master' into feat/pg-dsl
bsuehling Mar 20, 2024
5e64685
feat: add cli stuff
bsuehling Mar 21, 2024
392972c
fix: add missing field 'represents_fault' to json output
bsuehling Mar 21, 2024
71d64a1
chore: add pgdsl linux build
bsuehling Mar 21, 2024
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Next Next commit
[WIP] implement custom dsl
bsuehling committed Mar 9, 2024
commit c9e6d3946fd1e6202ba852592ab28adcfb9c0ecb
109 changes: 109 additions & 0 deletions pg-dsl/AST.hs
Original file line number Diff line number Diff line change
@@ -0,0 +1,109 @@
module AST
( AST
, PG(..)
, State
, VarDef
, Var
, Range(..)
, Value(..)
, Trans(..)
, Action
, Assign
, Expression(..)
, Term(..)
, Formula(..)
, Proposition
, RelOp(..)
, PError(..)
) where

type AST = Either PError PG

data PG = PG
{ name :: String
, variables :: [VarDef]
, states :: [State]
, transitions :: [Trans]
, initialState :: State
, initialFormula :: Formula
} deriving (Show, Eq)

type State = String

type VarDef = (String, Range)

type Var = String

data Range
= RBool
| RInt Int Int -- lower and upper bound
| REnum [String]
| RState
deriving (Show, Eq)

data Value
= VBool Bool
| VInt Int
| VEnum String
| VState State
deriving (Show, Eq)

data Trans = Trans
{ preState :: State
, guard :: Formula
, action :: Action
, postState :: State
} deriving (Show, Eq)

type Action = [Assign]

type Assign = (Var, Expression)

data Expression
= Arithmetic Term
| Boolean Formula
| Single String -- single variables cannot be categorized w/o context
deriving (Show, Eq)

data Term
= TermVar String
| Const Int
| Negative Term
| Add Term Term
| Subtract Term Term
| Multiply Term Term
| Divide Term Term
deriving (Show, Eq)

data Formula
= FTrue
| FFalse
| Prop Proposition
| Not Formula
| And Formula Formula
| Or Formula Formula
| Implies Formula Formula
| Equiv Formula Formula
deriving (Show, Eq)

type Proposition = (RelOp, Term, Term)

data RelOp
= Equal
| NotEqual
| Lower
| LowerEqual
| Greater
| GreaterEqual
deriving (Show, Eq)

data PError = PError
{ pMsg :: String
, pLine :: Int
, pCol :: Int
}

instance Show PError where
show :: PError -> String
show e =
pMsg e ++ " at line " ++ show (pLine e) ++ ", column " ++ show (pCol e)
9 changes: 9 additions & 0 deletions pg-dsl/Main.hs
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
module Main where

import Tokenizer (tokenize)

main :: IO ()
main = do
input <- readFile "./robot.txt"
let tokens = tokenize input
print tokens
408 changes: 408 additions & 0 deletions pg-dsl/Parser.hs

Large diffs are not rendered by default.

131 changes: 131 additions & 0 deletions pg-dsl/Token.hs
Original file line number Diff line number Diff line change
@@ -0,0 +1,131 @@
module Token
( TokenList
, Token(..)
, DToken(..)
, TError(..)
) where

type TokenList = Either TError [DToken]

-- TODO: show original chars
data Token
= TEoF
| TSpace
| TComment String
| TNewline
| TBRacketL
| TBracketR
| TCurlyL
| TCurlyR
| TSquareL
| TSquareR
| TComma
| TSemicolon
| TDots
| TArrow
| TWalrus
| TColon
| TPlus
| TMinus
| TStar
| TSlash
| TEqual
| TNotEqual
| TLowerEq
| TLower
| TGreaterEq
| TGreater
| TNot
| TOr
| TAnd
| TImplies
| TEquiv
| TGraph
| TVars
| TStates
| TInit
| TTransitions
| TGuard
| TAction
| TBool
| TInt
| TEnum
| TState
| TTrue
| TFalse
| TNumber Int
| TNameLower String
| TNameUpper String

instance Show Token where
show :: Token -> String
show TEoF = "end of file"
show TSpace = "' '"
show (TComment c) = "'" ++ c ++ "'"
show TNewline = "'end of line'"
show TBRacketL = "'('"
show TBracketR = "')'"
show TCurlyL = "'{'"
show TCurlyR = "'}'"
show TSquareL = "'['"
show TSquareR = "']'"
show TComma = "','"
show TSemicolon = "';'"
show TDots = "'..'"
show TArrow = "'->'"
show TWalrus = "':='"
show TColon = "':'"
show TPlus = "'+'"
show TMinus = "'-'"
show TStar = "'*'"
show TSlash = "'/'"
show TEqual = "'='"
show TNotEqual = "'!='"
show TLowerEq = "'<='"
show TLower = "'<'"
show TGreaterEq = "'>='"
show TGreater = "'>'"
show TNot = "'!'"
show TOr = "'|'"
show TAnd = "'&'"
show TImplies = "'=>'"
show TEquiv = "'<=>'"
show TGraph = "'graph'"
show TVars = "'variables'"
show TStates = "'states'"
show TInit = "'init'"
show TTransitions = "'transitions'"
show TGuard = "'guard'"
show TAction = "'action'"
show TBool = "'bool'"
show TInt = "'int'"
show TEnum = "'enum'"
show TState = "'state'"
show TTrue = "'true'"
show TFalse = "'false'"
show (TNumber n) = show n
show (TNameLower s) = "'" ++ s ++ "'"
show (TNameUpper s) = "'" ++ s ++ "'"

data DToken = DToken
{ token :: Token
, line :: Int
, column :: Int
}

instance Show DToken where
show :: DToken -> String
show t =
"(" ++
show (token t) ++ ", " ++ show (line t) ++ ", " ++ show (column t) ++ ")"

data TError = TError
{ tMsg :: String
, tLine :: Int
, tCol :: Int
}

instance Show TError where
show :: TError -> String
show e =
tMsg e ++ " at line " ++ show (tLine e) ++ ", column " ++ show (tCol e)
142 changes: 142 additions & 0 deletions pg-dsl/Tokenizer.hs
Original file line number Diff line number Diff line change
@@ -0,0 +1,142 @@
module Tokenizer
( tokenize
) where

import Data.Char (isAlpha, isAscii, isAsciiLower, isAsciiUpper,
isNumber)
import Token (DToken (..), TError (..), Token (..), TokenList)

tokenize :: String -> TokenList
tokenize = tok [] 1 1

tok :: [DToken] -> Int -> Int -> String -> TokenList
tok acc l c "" = Right $ reverse $ dec TEoF l c : acc
tok acc l c p@(' ':_) =
let (c', p') = spaces c p
in tok (dec TSpace l c : acc) l c' p'
tok acc l c ('\r':'\n':p) = tok (dec TNewline l c : acc) (l + 1) 1 p
tok acc l c ('\n':p) = tok (dec TNewline l c : acc) (l + 1) 1 p
tok acc l c ('\r':p) = tok (dec TNewline l c : acc) (l + 1) 1 p
tok acc l c p@('#':_) =
let (c', p', s) = comment c p
in tok (dec (TComment s) l c : acc) l c' p'
tok acc l c ('(':p) = tok (dec TBRacketL l c : acc) l (c + 1) p
tok acc l c (')':p) = tok (dec TBracketR l c : acc) l (c + 1) p
tok acc l c ('{':p) = tok (dec TCurlyL l c : acc) l (c + 1) p
tok acc l c ('}':p) = tok (dec TCurlyR l c : acc) l (c + 1) p
tok acc l c ('[':p) = tok (dec TSquareL l c : acc) l (c + 1) p
tok acc l c (']':p) = tok (dec TSquareR l c : acc) l (c + 1) p
tok acc l c (',':p) = tok (dec TComma l c : acc) l (c + 1) p
tok acc l c (';':p) = tok (dec TSemicolon l c : acc) l (c + 1) p
tok acc l c ('.':'.':p) = tok (dec TDots l c : acc) l (c + 2) p
tok acc l c ('-':'>':p) = tok (dec TArrow l c : acc) l (c + 2) p
tok acc l c (':':'=':p) = tok (dec TWalrus l c : acc) l (c + 2) p
tok acc l c (':':p) = tok (dec TColon l c : acc) l (c + 1) p
tok acc l c ('+':p) = tok (dec TPlus l c : acc) l (c + 1) p
tok acc l c ('-':p) = tok (dec TMinus l c : acc) l (c + 1) p
tok acc l c ('*':p) = tok (dec TStar l c : acc) l (c + 1) p
tok acc l c ('/':p) = tok (dec TSlash l c : acc) l (c + 1) p
tok acc l c ('=':'>':p) = tok (dec TImplies l c : acc) l (c + 2) p
tok acc l c ('<':'=':'>':p) = tok (dec TImplies l c : acc) l (c + 3) p
tok acc l c ('=':p) = tok (dec TEqual l c : acc) l (c + 1) p
tok acc l c ('!':'=':p) = tok (dec TNotEqual l c : acc) l (c + 2) p
tok acc l c ('<':'=':p) = tok (dec TLowerEq l c : acc) l (c + 2) p
tok acc l c ('<':p) = tok (dec TLower l c : acc) l (c + 1) p
tok acc l c ('>':'=':p) = tok (dec TGreaterEq l c : acc) l (c + 2) p
tok acc l c ('>':p) = tok (dec TGreater l c : acc) l (c + 1) p
tok acc l c ('!':p) = tok (dec TNot l c : acc) l (c + 1) p
tok acc l c ('|':p) = tok (dec TOr l c : acc) l (c + 1) p
tok acc l c ('&':p) = tok (dec TAnd l c : acc) l (c + 1) p
tok acc l c p@('g':'r':'a':'p':'h':t)
| nextAlphaNum t = tokLower acc l c p
| otherwise = tok (dec TGraph l c : acc) l (c + 5) t
tok acc l c p@('v':'a':'r':'i':'a':'b':'l':'e':'s':t)
| nextAlphaNum t = tokLower acc l c p
| otherwise = tok (dec TVars l c : acc) l (c + 9) t
tok acc l c p@('s':'t':'a':'t':'e':'s':t)
| nextAlphaNum t = tokLower acc l c p
| otherwise = tok (dec TStates l c : acc) l (c + 6) t
tok acc l c p@('i':'n':'i':'t':t)
| nextAlphaNum t = tokLower acc l c p
| otherwise = tok (dec TInit l c : acc) l (c + 4) t
tok acc l c p@('t':'r':'a':'n':'s':'i':'t':'i':'o':'n':'s':t)
| nextAlphaNum t = tokLower acc l c p
| otherwise = tok (dec TTransitions l c : acc) l (c + 11) t
tok acc l c p@('g':'u':'a':'r':'d':t)
| nextAlphaNum t = tokLower acc l c p
| otherwise = tok (dec TGuard l c : acc) l (c + 5) t
tok acc l c p@('a':'c':'t':'i':'o':'n':t)
| nextAlphaNum t = tokLower acc l c p
| otherwise = tok (dec TAction l c : acc) l (c + 6) t
tok acc l c p@('b':'o':'o':'l':t)
| nextAlphaNum t = tokLower acc l c p
| otherwise = tok (dec TBool l c : acc) l (c + 4) t
tok acc l c p@('i':'n':'t':t)
| nextAlphaNum t = tokLower acc l c p
| otherwise = tok (dec TInt l c : acc) l (c + 3) t
tok acc l c p@('e':'n':'u':'m':t)
| nextAlphaNum t = tokLower acc l c p
| otherwise = tok (dec TEnum l c : acc) l (c + 4) t
tok acc l c p@('s':'t':'a':'t':'e':t)
| nextAlphaNum t = tokLower acc l c p
| otherwise = tok (dec TState l c : acc) l (c + 5) t
tok acc l c p@('t':'r':'u':'e':t)
| nextAlphaNum t = tokLower acc l c p
| otherwise = tok (dec TTrue l c : acc) l (c + 4) t
tok acc l c p@('f':'a':'l':'s':'e':t)
| nextAlphaNum t = tokLower acc l c p
| otherwise = tok (dec TFalse l c : acc) l (c + 1) t
tok acc l c p@(x:_)
| isNumber x =
let (c', p', n) = readNumber c p
in tok (dec (TNumber n) l c : acc) l c' p'
| isAsciiUpper x =
let (c', p', s) = readName c p
in tok (dec (TNameUpper s) l c : acc) l c' p'
| isAsciiLower x = tokLower acc l c p
| otherwise =
Left $ TError {tMsg = "Invalid char: " ++ show x, tLine = l, tCol = c}

tokLower :: [DToken] -> Int -> Int -> String -> TokenList
tokLower acc l c p =
let (c', p', s) = readName c p
in tok (dec (TNameLower s) l c : acc) l c' p'

spaces :: Int -> String -> (Int, String)
spaces i (' ':s) = spaces (i + 1) s
spaces i s = (i, s)

comment :: Int -> String -> (Int, String, String)
comment = comment' ""
where
comment' :: String -> Int -> String -> (Int, String, String)
comment' acc i s@('\r':'\n':_) = (i, s, reverse acc)
comment' acc i s@('\r':_) = (i, s, reverse acc)
comment' acc i s@('\n':_) = (i, s, reverse acc)
comment' acc i (c:s) = comment' (c : acc) (i + 1) s

readNumber :: Int -> String -> (Int, String, Int)
readNumber = readNumber' ""
where
readNumber' :: String -> Int -> String -> (Int, String, Int)
readNumber' acc i p@(x:xs)
| isNumber x = readNumber' (x : acc) (i + 1) xs
| otherwise = (i, p, read $ reverse acc)

readName :: Int -> String -> (Int, String, String)
readName = readName' ""
where
readName' :: String -> Int -> String -> (Int, String, String)
readName' acc i p@(x:xs)
| isAsciiAlphaNum x = readName' (x : acc) (i + 1) xs
| otherwise = (i, p, reverse acc)

nextAlphaNum :: String -> Bool
nextAlphaNum "" = False
nextAlphaNum s = isAsciiAlphaNum $ head s

isAsciiAlphaNum :: Char -> Bool
isAsciiAlphaNum x = isAscii x && (isAlpha x || isNumber x)

dec :: Token -> Int -> Int -> DToken
dec t l c = DToken {token = t, line = l, column = c}
21 changes: 21 additions & 0 deletions pg-dsl/backup.txt
Original file line number Diff line number Diff line change
@@ -0,0 +1,21 @@
pg2 name (h:t) =
case token h of
TCurlyL ->
let (vars, p1) = pVars t
(sts, p2) = pStates p1
((initS, initF), p3) = pInit p2
(trs, p4) = pTrans p3
in case token (head p4) of
TCurlyR ->
Right
( PG
{ name = name
, variables = vars
, states = sts
, transitions = trs
, initialState = initS
, initialFormula = initF
}
, tail p4)
_ -> Left $ raise TCurlyR $ head p4
_ -> Left $ raise TCurlyL h
48 changes: 48 additions & 0 deletions pg-dsl/example.txt
Original file line number Diff line number Diff line change
@@ -0,0 +1,48 @@
graph Robot {
Vars {
int num [0..7]
state LightBarrier
}

states { Idle, Busy, Inactive }

init: Idle { num = 0 }

transitions {
Idle -> Busy {
guard { LightBarrier = Signal }
action { num := num + 1 }
}

Busy -> Idle {
guard { num < 3 }
}

Busy -> Busy {}

Busy -> Inactive {
guard { num = 3 }
}
}
}

graph LightBarrier {
states { Idle, Signal }

init: Idle {}

transitions {
Idle -> Idle {}

Idle -> Signal {}

Signal -> Idle {}

Signal -> Signal {}
}
}

main {
Robot,
LightBarrier
}
28 changes: 28 additions & 0 deletions pg-dsl/robot.txt
Original file line number Diff line number Diff line change
@@ -0,0 +1,28 @@
graph Robot {
vars {
int num [0..7]
state LightBarrier
}

# Here, we define the states
states { Idle, Busy, Inactive }

init: Idle { num = 0 }

transitions {
Idle -> Busy {
guard { LightBarrier = Signal }
action { num := num + 1 }
}

Busy -> Idle {
guard { num < 3 } # cause why not
}

Busy -> Busy {}

Busy -> Inactive {
guard { num = 3 }
}
}
}