syfco-1.1.0.0: src/Info.hs
-----------------------------------------------------------------------------
-- |
-- Module : Info
-- License : MIT (see the LICENSE file)
-- Maintainer : Felix Klein (klein@react.uni-saarland.de)
--
-- Several printers to report information back to the user.
--
-----------------------------------------------------------------------------
{-# LANGUAGE
LambdaCase
, MultiParamTypeClasses
, TypeSynonymInstances
, FlexibleContexts
#-}
-----------------------------------------------------------------------------
module Info
( prTitle
, prDescription
, prSemantics
, prTarget
, prTags
, prInfo
, prParameters
, prInputs
, prOutputs
, prVersion
, prHelp
, prReadme
, prReadmeMd
, prError
) where
-----------------------------------------------------------------------------
import Syfco
( Configuration(..)
, Semantics(..)
, Target(..)
, WriteFormat(..)
, WriteMode(..)
, Specification
, defaultCfg
, title
, description
, semantics
, target
, tags
, parameters
, inputs
, outputs
, version
)
import Data.Convertible
( Convertible
, convert
)
import Data.Array
( (!)
)
import Control.Monad
( unless
)
import System.Exit
( exitFailure
)
import System.IO
( hPutStrLn
, stderr
)
-----------------------------------------------------------------------------
data Mode = Plain | Help | Markdown
-----------------------------------------------------------------------------
-- | Prints the title of the given specification.
prTitle
:: Specification -> IO ()
prTitle s =
putStrLn $ title s
-----------------------------------------------------------------------------
-- | Prints the description of the given specification.
prDescription
:: Specification -> IO ()
prDescription s =
putStrLn $ description s
-----------------------------------------------------------------------------
-- | Prints the semantics of the given specification.
prSemantics
:: Specification -> IO ()
prSemantics s =
putStrLn $ case semantics s of
SemanticsMealy -> "Mealy"
SemanticsMoore -> "Moore"
SemanticsStrictMealy -> "Strict,Mealy"
SemanticsStrictMoore -> "Strict,Moore"
-----------------------------------------------------------------------------
-- | Prints the target of the given specification.
prTarget
:: Specification -> IO ()
prTarget s =
putStrLn $ case target s of
TargetMealy -> "Mealy"
TargetMoore -> "Moore"
-----------------------------------------------------------------------------
-- | Prints the tag list of the given specification.
prTags
:: Specification -> IO ()
prTags s = case tags s of
[] -> return ()
xs -> putStrLn $ head xs ++ concatMap ((:) ' ' . (:) ',') (tail xs)
-----------------------------------------------------------------------------
-- | Prints the parameters of the given specification.
prParameters
:: Specification -> IO ()
prParameters s = putStrLn $ case parameters s of
(x:xr) -> x ++ concatMap ((:) ',' . (:) ' ') xr
[] -> ""
-----------------------------------------------------------------------------
-- | Prints the input signals of the given specification.
prInputs
:: Configuration -> Specification -> IO ()
prInputs c s = case inputs c s of
Left err -> prError $ show err
Right (x:xr) -> putStrLn $ x ++ concatMap ((:) ',' . (:) ' ') xr
_ -> return ()
-----------------------------------------------------------------------------
-- | Prints the output signals of the given specification.
prOutputs
:: Configuration -> Specification -> IO ()
prOutputs c s = case outputs c s of
Left err -> prError $ show err
Right (x:xr) -> putStrLn $ x ++ concatMap ((:) ',' . (:) ' ') xr
_ -> return ()
-----------------------------------------------------------------------------
-- | Prints the complete INFO section of the given specification.
prInfo
:: Specification -> IO ()
prInfo s = do
putStrLn $ "Title: \"" ++ title s ++ "\""
putStrLn $ "Description: \"" ++ description s ++ "\""
putStr "Semantics: "
prSemantics s
putStr "Target: "
prTarget s
unless (null $ tags s) $ do
putStr "Tags: "
prTags s
-----------------------------------------------------------------------------
-- | Prints the version and the program name.
prVersion
:: IO ()
prVersion = do
putStrLn $ "SyFCo (v" ++ version ++ ")"
putStrLn "The Synthesis Format Converter"
-----------------------------------------------------------------------------
-- | Prints the help of the program.
prHelp
:: IO ()
prHelp = putStr $ usage Help
-----------------------------------------------------------------------------
-- | Prints the content of the README file.
prReadme
:: IO ()
prReadme = putStr $ readme Plain
-----------------------------------------------------------------------------
-- | Prints the content of the README.md file.
prReadmeMd
:: IO ()
prReadmeMd = putStr $ readme Markdown
-----------------------------------------------------------------------------
usage
:: Mode -> String
usage m =
unlines $
[ switch "## Usage\n\n" "Usage: " "## Usage\n\n" ++
code m ("syfco [OPTIONS]... <file>") ++
switch "\n" ("\n\nA Synthesis Format Converter to read and " ++
"transform Temporal Logic\nSpecification Format " ++
"(TLSF) files.") "" ] ++
section "File Operations" (prTable foTable) ++
section "File Modifications" (prTable fmTable) ++
section ("Formula Transformations " ++
"(disabled by default)") (prTable ftTable) ++
section "Check Specification Type (and exit)" (prTable csTable) ++
section "Extract Information (and exit)" (prTable eiTable) ++
section "Sample Usage" sample
where
idl (s1,s2,_,_) = length s1 + length s2 + 7
len = foldl max 0 $
[ foldl max 0 $ map idl foTable
, foldl max 0 $ map idl fmTable
, foldl max 0 $ map idl ftTable
, foldl max 0 $ map idl csTable
, foldl max 0 $ map idl eiTable ]
switch s1 s2 s3 = case m of
Plain -> s1
Help -> s2
Markdown -> s3
section h xs = [ "", ind ++ h ++ ":", "" ] ++ xs
ind = case m of
Plain -> "### "
Help -> ""
Markdown -> "#### "
wrap str = case m of
Markdown -> code m str
_ -> "`" ++ str ++ "`"
sample = [ codeblock m $ map (("syfco ") ++)
[ "-o converted -f promela -m fully -nnf -nd file.tlsf"
, "-f psl -op n=3 -os Strict,Mealy -o converted file.tlsf"
, "-o converted -in"
, "-t file.tlsf" ] ]
prTable xs =
let xs' =
map (\(x,y,z,vs) ->
(x,y,adaptsub (80 - len - 3) z,
adapt (80 - len - 3) vs)) xs
in case m of
Markdown ->
[ "|Command|Description|"
, "|-------|-----------|" ]
++ map prMRow (filter (\(s,_,_,_) -> not $ null s) xs')
_ ->
concatMap prRow xs'
adaptsub l c = case c of
Nothing -> Nothing
Just xs -> Just $ map (\(a,b,c) -> (a,b,adapt l c)) xs
adapt
:: Int -> [String] -> [String]
adapt l xs = concatMap (adapt' l) xs
adapt' l str
| length str <= l = [str]
| otherwise = case m of
Markdown -> [str]
_ -> rearrange l [] [] 0 $ words str
rearrange l a b n [] =
reverse ((unwords $ reverse b):a)
rearrange l a [] _ (x:xr)
| length x > l = rearrange l (x:a) [] 0 xr
| otherwise = rearrange l a [x] (length x) xr
rearrange l a b n (x:xr)
| n + length x + 1 > l =
rearrange l ((unwords $ reverse b):a) [x] (length x) xr
| otherwise = rearrange l a (x:b) (n + length x + 1) xr
prMRow (short,long,sub,desc) =
"|" ++ code m ("-" ++ short ++ ", --" ++ long) ++ "|" ++
( case desc of
[] -> ""
x:xr -> concat (x : map ("</br> " ++) xr) ++
case sub of
Nothing -> ""
Just ys -> "</br> <table><tbody> " ++
concatMap prMSub ys ++
" </tbody></table>"
) ++ "|"
prMSub (name,d,desc) =
"<tr><td>" ++ code m name ++
"</td><td>" ++ concat (addbreaks desc) ++
(if d then " (default)" else "") ++
"</td></tr>"
addbreaks xs = case xs of
[] -> []
x:xr -> x : map ("</br>" ++) xr
prRow (short,long,sub,desc)
| short == "" = [ "" ]
| otherwise = case desc of
[] ->
prRow (short,long,sub,[""])
x:xr ->
( ( " -" ++ short ++ ", --" ++ long ++
replicate (len - (length short + length long + 7)) ' '
++ " : " ++ x)
: ( [ replicate (len + 3) ' ' ++ y | y <- xr ] ++
(case sub of
Nothing -> []
Just ys -> [""] ++ concatMap prSub ys ++ [""] ) ) )
prSub (n,d,desc) = case desc of
[] -> prSub (n,d,[""])
x:xr ->
(" * " ++ n ++
(if d then
" [default]" ++ replicate (len - 16 - length n) ' '
else
replicate (len - 6 - length n) ' ') ++
" : " ++ x) :
map ((replicate (len+3) ' ') ++) xr
foTable =
[ ("o", "output", Nothing,
[ "path of the output file (results are printed " ++
"to STDOUT if not set)" ])
, ("r", "read-config", Nothing,
[ "read parameters from the given configuration file (may " ++
"overwrite prior arguments)" ])
, ("w", "write-config", Nothing,
[ "write the current configuration to the given path " ++
"(includes later arguments)" ])
, ("f", "format", Just formats,
[ "output format - possible values are:" ])
, ("m", "mode", Just modes,
[ "output mode - possible values are:" ])
, ("pf", "part-file", Nothing,
[ "create a partitioning (" ++ code m ".part" ++ ") file" ])
, ("bd", "bus-delimiter", Nothing,
[ "delimiter used to print indexed bus signals",
"(default: "++ wrap (busDelimiter defaultCfg) ++ ")" ])
, ("ps", "prime-symbol", Nothing,
[ "symbol/string denoting primes in signals",
"(default: " ++ wrap (primeSymbol defaultCfg) ++ ")" ])
, ("as", "at-symbol", Nothing,
[ "symbol/string denoting @-symbols in signals",
"(default: " ++ wrap (atSymbol defaultCfg) ++ ")" ])
, ("in", "stdin", Nothing,
[ "read the input file from STDIN" ]) ]
fmTable =
[ ("os", "overwrite-semantics", Nothing,
[ "overwrite the semantics of the file" ])
, ("ot", "overwrite-target", Nothing,
[ "overwrite the target of the file" ])
, ("op", "overwrite-parameter", Nothing,
[ "overwrite a parameter of the file" ]) ]
ftTable =
[ ("s0", "weak-simplify", Nothing,
[ "simple simplifications (removal of true/false " ++
"in boolean connectives, redundant temporal " ++
"operators, etc.)" ])
, ("s1", "strong-simplify", Nothing,
[ "advanced simplifications",
"(includes: " ++
code m "-s0 -nnf -nw -nr -pgo -pfo -pxo" ++ ")" ])
, ("nnf", "negation-normal-form", Nothing,
[ "convert the resulting LTL formula into negation " ++
"normal form" ])
, ("pgi", "push-globally-inwards", Nothing,
[ "push global operators inwards",
" " ++ code m "G (a && b) => (G a) && (G b)" ])
, ("pfi", "push-finally-inwards", Nothing,
[ "push finally operators inwards",
" " ++ code m "F (a || b) => (F a) || (F b)" ])
, ("pxi", "push-next-inwards", Nothing,
[ "push next operators inwards",
" " ++ code m "X (a && b) => (X a) && (X b)",
" " ++ code m "X (a || b) => (X a) || (X b)" ])
, ("pgo", "pull-globally-outwards", Nothing,
[ "pull global operators outwards",
" " ++ code m "(G a) && (G b) => G (a && b)" ])
, ("pfo", "pull-finally-outwards", Nothing,
[ "pull finally operators outwards",
" " ++ code m "(F a) || (F b) => F (a || b)" ])
, ("pxo", "pull-next-outwards", Nothing,
[ "pull next operators outwards",
" " ++ code m "(X a) && (X b) => X (a && b)",
" " ++ code m "(X a) || (X b) => X (a || b)" ])
, ("nw", "no-weak-until", Nothing,
[ "replace weak until operators",
" " ++ code m "a W b => (a U b) || (G a)" ])
, ("nr", "no-release", Nothing,
[ "replace release operators",
" " ++ code m "a R b => b W (a && b)" ])
, ("nf", "no-finally", Nothing,
[ "replace finally operators",
" " ++ code m "F a => true U a" ])
, ("ng", "no-globally", Nothing,
[ "replace global operators",
" " ++ code m "G a => false R a" ])
, ("nd", "no-derived", Nothing,
[ "same as: " ++ code m "-nw -nf -ng" ]) ]
csTable =
[ ("gr", "generalized-reactivity", Nothing,
[ "check whether the input is in the " ++
"Generalized Reactivity fragment" ]) ]
eiTable =
[ ("c", "check", Nothing,
[ "check that input conforms to TLSF" ])
, ("t", "print-title", Nothing,
[ "output the title of the input file" ])
, ("d", "print-description", Nothing,
[ "output the description of the input file" ])
, ("s", "print-semantics", Nothing,
[ "output the semantics of the input file" ])
, ("g", "print-target", Nothing,
[ "output the target of the input file" ])
, ("a", "print-tags", Nothing,
[ "output the target of the input file" ])
, ("p", "print-parameters", Nothing,
[ "output the parameters of the input file" ])
, ("i", "print-info", Nothing,
[ "output all data of the info section" ])
, ("ins", "print-input-signals", Nothing,
[ "output the input signals of the specification" ])
, ("outs", "print-output-signals", Nothing,
[ "output the output signals of the specification" ])
, ("","", Nothing,
[])
, ("v", "version", Nothing,
[ "output version information" ])
, ("h", "help", Nothing,
[ "display this help" ]) ]
formats =
[ (convert FULL, True,
["input file with applied transformations"])
, (convert BASIC, False,
["high level format (without global section)"])
, (convert UTF8, False,
["human readable output using UTF8 symbols"])
, (convert WRING, False,
["Wring input format"])
, (convert LILY, False,
["Lily input format"])
, (convert ACACIA, False,
["Acacia / Acacia+ input format"])
, (convert ACACIASPECS, False,
["Acacia input format with spec units"])
, (convert LTLXBA, False,
["LTL2BA / LTL3BA input format"])
, (convert PROMELA, False,
["Promela LTL"])
, (convert UNBEAST, False,
["Unbeast input format"])
, (convert SLUGS, False,
["structured Slugs format [GR(1) only]"])
, (convert SLUGSIN, False,
["SlugsIn format [GR(1) only]"])
, (convert PSL, False,
["PSL Syntax"])
, (convert SMV, False,
["SMV file format"])
, (convert BOSY, False,
["Bosy input format"])
]
modes =
[ (convert Pretty, True,
["pretty printing (as less parentheses as possible)"])
, (convert Fully, False,
["output fully parenthesized formulas"]) ]
-----------------------------------------------------------------------------
readme
:: Mode -> String
readme m = appendlinks $ unlines
[ switch
("# Synthesis Format Conversion Tool\n# (Version " ++
version ++ ")")
("# Synthesis Format Conversion Tool<br/>(Version " ++
version ++ ")")
, ""
, "A tool for reading, manipulating and transforming synthesis"
, "specifications in " ++
link "TLSF" "https://arxiv.org/abs/1604.02284" ++ "."
, ""
, "## About this tool"
, ""
, "The tool interprets the high level constructs of " ++
link "TLSF 1.1" "https://arxiv.org/abs/1604.02284"
, "(functions, sets, ...) and supports the transformation of the"
, "specification to Linear Temporal Logic (LTL) in different output"
, "formats. The tool has been designed to be modular with respect to the"
, "supported output formats and semantics. Furthermore, the tool allows"
, "to identify and manipulate parameters, targets and semantics of a"
, "specification on the fly. This is especially thought to be useful for"
, "comparative studies, as they are for example needed in the"
, link "Synthesis Competition" "http://www.syntcomp.org" ++ "."
, ""
, "The main features of the tool are summarized as follows:"
, ""
, "* Interpretation of high level constructs, which allows to reduce the"
, " specification to its basic fragment where no more parameter and"
, " variable bindings occur (i.e., without the GLOBAL section)."
, ""
, "* Transformation to other existing specification formats, like"
, " Basic TLSF, " ++
link "Promela LTL" "http://spinroot.com/spin/Man/ltl.html" ++ ", " ++
link "PSL" ("https://en.wikipedia.org/wiki/" ++
"Property_Specification_Language")
++ ", " ++
link "Unbeast" "https://www.react.uni-saarland.de/tools/unbeast"
++ ", " ++
link "Wring" "http://www.ist.tugraz.at/staff/bloem/wring.html"
++ ","
, " " ++
link "structured Slugs"
("https://github.com/VerifiableRobotics/slugs/" ++
"blob/master/doc/input_formats.md#structuredslugs")
++ ", and " ++ link "SlugsIn"
("https://github.com/VerifiableRobotics/slugs/blob/master/" ++
"doc/input_formats.md#slugsin") ++ "."
, ""
, "* Syntactical analysis of membership in GR(k) for any k (modulo"
, " Boolean identities)."
, ""
, "* On the fly adjustment of parameters, semantics or targets."
, ""
, "* Preprocessing of the resulting LTL formula."
, ""
, "* Conversion to negation normal form."
, ""
, "* Replacement of derived operators."
, ""
, "* Pushing/pulling next, eventually, or globally operators"
, " inwards/outwards."
, ""
, "* Standard simplifications."
, switch "\n" ""
, "## Installation"
, ""
, "SyfCo is written in Haskell and can be compiled using the"
, "Glasgow Haskell Compiler (GHC). To install the tool you can either"
, "use " ++ link "cabal" "https://www.haskell.org/cabal" ++ " or " ++
link "stack" "https://docs.haskellstack.org/en/stable/README/" ++
" (recommended)."
, "For more information about the purpose of these tools and why you"
, "should prefer using stack instead of cabal, we recommend reading"
, link "this blog post"
"https://www.fpcomplete.com/blog/2015/06/why-is-stack-not-cabal" ++
" by Mathieu Boespflug. "
, ""
, "To install the tool with stack use:"
, ""
, scb "stack install"
, ""
, "Stack then automatically fetches the right compiler version"
, "and required dependencies. After that it builds and installs"
, "the package into you local stack path. If you instead prefer"
, "to build only, use `stack build`."
, ""
, "If you insist to use cabal instead, we recommend at least to use"
, "a sandbox. Initialize the sandbox and configure the project via"
, ""
, scb "cabal sandbox init && cabal configure"
, ""
, "Then use `cabal build` or `cabal install` to build or install the"
, "tool."
, ""
, "Note that (independent of the chosen build method) building the"
, "tool will only create the final executable in a hidden sub-folder,"
, "which might get cumbersome for development or testing local changes."
, "Hence, for this purpose, you may prefer to use `make`. The makefile"
, "determines the chosen build method, rebuilds the package, and copies"
, "the final `syfco` executable to the root directory of the project."
, ""
, "If you still encounter any problems, please inform us via the"
, switch
("project bug tracker:\n\n " ++
"https://github.com/reactive-systems/syfco/issues\n\n")
(link "project bug tracker"
"https://github.com/reactive-systems/syfco/issues"
++ ".\n")
, usage m
, "## Examples"
, ""
, "A number of synthesis benchmarks in TLSF can be found in the"
, code m "/examples" ++ " directory."
, ""
, "## Syfco Library"
, ""
, "Syfco is also provided as a Haskell library. In fact, the syfco"
, "executable is nothing different than a fancy command line interface"
, "to this library. If you are interested in using the interface, we"
, "recommend to build and check the interface documentation, which is"
, "generated by:"
, ""
, scb "make haddock"
, ""
, "## Editor Support"
, ""
, "If you use " ++ link "Emacs" "https://www.gnu.org/software/emacs" ++
", you should try our emacs mode (" ++ code m "tlsf-mode.el" ++ "),"
, "which can be found in the " ++ code m "/misc" ++ " directory."
, ""
, "## Adding output formats"
, ""
, "If you like to add a new output format, first consider"
, code m "/Writer/Formats/Example.hs" ++
", which contains the most common"
, "standard constructs and a short tutorial." ]
where
scb str = case m of
Markdown -> "`" ++ str ++ "`"
_ -> " " ++ str
switch s1 s2 = case m of
Markdown -> s2
_ -> s1
link n url = "[" ++ n ++ "](" ++ url ++ ")"
appendlinks str = case m of
Markdown -> str
_ ->
let (str',ls) = replclct [] [] [] [] 0 0 str
in str' ++
"\n--------------------------------------------------\n\n" ++
concatMap (\(n,s1,s2) -> "[" ++ show n ++ "]" ++
replicate (4 - length (show n)) ' '
++ s2 ++ "\n") ls
replclct a b c1 c2 n m xs = case xs of
[] -> case m of
0 -> (reverse b, reverse a)
1 -> (reverse (c1 ++ ('[' : b)), reverse a)
2 -> (reverse (('(' : ']' : c1) ++ ('[' : b)), reverse a)
_ -> (reverse (c2 ++ ('(' : ']' : c1) ++ ('[' : b)), reverse a)
x:xr -> case (x,m) of
('[',0) -> replclct a b c1 c2 n 1 xr
( _ ,0) -> replclct a (x:b) c1 c2 n 0 xr
(']',1) -> replclct a b c1 c2 n 2 xr
( _ ,1) -> replclct a b (x:c1) c2 n 1 xr
('(',2) -> replclct a b c1 c2 n 3 xr
( _ ,2) -> replclct a (x:(']':c1) ++ ('[': b)) [] [] n 0 xr
(')',_) -> replclct ((n,reverse c1, reverse c2):a)
((']' : reverse (show n)) ++ ('[' : ' ' : c1) ++ b)
[] [] (n+1) 0 xr
( _ ,_) -> replclct a b c1 (x:c2) n 3 xr
-----------------------------------------------------------------------------
code
:: Mode -> String -> String
code m str = case m of
Markdown -> "```" ++ str ++ "```"
_ -> str
-----------------------------------------------------------------------------
codeblock
:: Mode -> [String] -> String
codeblock m xs = case m of
Markdown -> "```\n" ++ unlines xs ++ "```\n"
_ -> unlines $ map ((' ':) . (' ':)) xs
-----------------------------------------------------------------------------
-- | Prints an error to STDERR and then terminates the program.
prError
:: String -> IO a
prError err = do
hPutStrLn stderr err
exitFailure
-----------------------------------------------------------------------------