License	MIT (see the LICENSE file)
Maintainer	Felix Klein (klein@react.uni-saarland.de)
Safe Haskell	None
Language	Haskell2010

Syfco

Contents

Data Structures
Configurations
Specifcations
Fragment Detection
Meta Information

Description

Syfco Library Interface.

Synopsis

Data Structures

data Configuration Source #

The data type contains all flags and settings that can be adjusted to influence the behavior of the library:

Constructors

Configuration

Fields

inputFiles :: [FilePath]
The list of input files containing the specifications.
outputFile :: Maybe FilePath
An optional path to the output file, the transformed specification is written to.
outputFormat :: WriteFormat
The format specifiying the corresponding writer to use.
(can be changed via a configuration file, use: format = ... )
outputMode :: WriteMode
The output mode used by the writer.
(can be changed via a configuration file, use: mode = ... )
partFile :: Maybe String
Optional path to a parition file, which is created if set.
busDelimiter :: String
The delimiter string to seperate the bus index from the signal name.
(can be changed via a configuration file, use: bus_delimiter = ... )
primeSymbol :: String
The prime symbol / string representing primes in signals of the input format.
(can be changed via a configuration file, use: prime_symbol = ... )
atSymbol :: String
The at symbol / string representing at symbols in signals of the input format.
(can be changed via a configuration file, use: at_symbol = ... )
fromStdin :: Bool
A boolean flag specifying whether the input should be read from STDIN or not.
owSemantics :: Maybe Semantics
An optional flag which allows to overwrite the semantics of the given input specifications.
(can be changed via a configuration file, use: overwrite_semantics = ... )
owTarget :: Maybe Target
An optional flag which allows to overwrite the target of the given input specifications.
(can be changed via a configuration file, use: overwrite_target = ... )
owParameter :: [(String, Int)]
An optional flag which allows to overwrite a list of parameters of the given input specification.
simplifyWeak :: Bool
A boolean flag specifying whether weak simplifications should be applied or not.
(can be changed via a configuration file, use: weak_simplify = ... )
simplifyStrong :: Bool
A boolean flag specifying whether strong simplifications should be applied or not.
(can be changed via a configuration file, use: strong_simplify = ... )
negNormalForm :: Bool
A boolean flag specifying whether the given specification should be turned into negation normal form.
(can be changed via a configuration file, use: negation_normal_form = ... )
pushGlobally :: Bool
A boolean flag specifying whether globally operators should be pushed over conjunctions deeper into the formula.
(can be changed via a configuration file, use: push_globally_inwards = ... )
pushFinally :: Bool
A boolean flag specifying whether finally operators should be pushed over disjunctions deeper into the formula.
(can be changed via a configuration file, use: push_finally_inwards = ... )
pushNext :: Bool
A boolean flag specifying whether next operators should be pushed over conjunctions and disjunctions deeper into the formula.
(can be changed via a configuration file, use: push_next_inwards = ... )
pullGlobally :: Bool
A boolean flag specifying whether globally perators should be pulled over conjunctions outside the formula.
(can be changed via a configuration file, use: pull_globally_outwards = ... )
pullFinally :: Bool
A boolean flag specifying whether finally operators should be pulled over disjunctions outside the formula.
(can be changed via a configuration file, use: pull_finally_outwards = ... )
pullNext :: Bool
A boolean flag specifying whether next operators should be pulled over conjunctions and disjunctions outside the formula.
(can be changed via a configuration file, use: pull_next_outwards = ... )
noWeak :: Bool
A boolean flag specifying whether weak until operators should be replaced by alternative operators inside the created formula.
(can be changed via a configuration file, use: no_weak_until = ... )
noRelease :: Bool
A boolean flag specifying whether release operators should be replaced by alternative operators inside the created formula.
(can be changed via a configuration file, use: no_release = ... )
noFinally :: Bool
A boolean flag specifying whether finally operators should be replaced by alternative operators inside the created formula.
(can be changed via a configuration file, use: no_finally = ... )
noGlobally :: Bool
A boolean flag specifying whether globally operators should be replaced by alternative operators inside the created formula.
(can be changed via a configuration file, use: no_globally = ... )
noDerived :: Bool
A boolean flag specifying whether any derived operators should be replaced by alternative operators inside the created formula.
(can be changed via a configuration file, use: no_derived = ... )
cGR :: Bool
A boolean flag specifying whether to check, whether the input belongs to the class of Generalized Reactivity specifications or not.
check :: Bool
A boolean flag specifying whether the given input files should just be checked for syntactical and type correctenss.
pTitle :: Bool
A boolean flag specifying whether just the title of the given input files should be printed or not.
pDesc :: Bool
A boolean flag specifying whether just the description of the given input files should be printed or not.
pSemantics :: Bool
A boolean flag specifying whether just the semantics of the given input files should be printed or not.
pTarget :: Bool
A boolean flag specifying whether just the target of the given input files should be printed or not.
pTags :: Bool
A boolean flag specifying whether just the tag list of the given input files should be printed or not,
pParameters :: Bool
A boolean flag specifying whether just the parameter list of the given specification should be printed or not.
pInputs :: Bool
A boolean flag specifying whether just the input signals of the given specification should be printed or not.
pOutputs :: Bool
A boolean flag specifying whether just the output signals of the given specification should be printed or not.
pInfo :: Bool
A boolean flag specifying whether just the complete input section of the given input files should be printed or not.
pVersion :: Bool
A boolean flag specifying whether the version info should be printed or not.
pHelp :: Bool
A boolean flag specifying whether the help info should be printed or not.
pReadme :: Bool
A boolean flag specifying whether the content of the README file should be printed to STDOUT or not.
pReadmeMd :: Bool
A boolean flag specifying whether the content of the README.md file should be printed to STDOUT or not.
saveConfig :: [FilePath]
List of file paths to store the current configuration.

Instances

Eq Configuration Source #
Methods (==) :: Configuration -> Configuration -> Bool # (/=) :: Configuration -> Configuration -> Bool #
Ord Configuration Source #
Methods compare :: Configuration -> Configuration -> Ordering # (<) :: Configuration -> Configuration -> Bool # (<=) :: Configuration -> Configuration -> Bool # (>) :: Configuration -> Configuration -> Bool # (>=) :: Configuration -> Configuration -> Bool # max :: Configuration -> Configuration -> Configuration # min :: Configuration -> Configuration -> Configuration #
Convertible Configuration String Source #	Creates the content of a parsable configuration file restricted to supported configuration file parameters.
Methods safeConvert :: Configuration -> ConvertResult String #

data WriteFormat Source #

Supported writer formats.

Constructors

UTF8	human readable output using UTF8 symbols
FULL	full format including all extensions
BASIC	basic format restricted to pure LTL formulas
WRING	http://www.ist.tugraz.at/staff/bloem/wring.html
PROMELA	http://spinroot.com/spin/Man/ltl.html
UNBEAST	https://www.react.uni-saarland.de/tools/unbeast
LTLXBA	LTL2BA / LTL3BA input format
LILY	Lily input format
ACACIA	Acacia / Acacia+ input format
ACACIASPECS	Acacia input format with spec units
SLUGS	https://github.com/VerifiableRobotics/slugs/blob/master/doc/input_formats.md#structuredslugs
SLUGSIN	https://github.com/VerifiableRobotics/slugs/blob/master/doc/input_formats.md#slugsin
PSL	https://en.wikipedia.org/wiki/Property_Specification_Language
SMV	SMV file format
BOSY	https://github.com/reactive-systems/bosy

Instances

Eq WriteFormat Source #
Methods (==) :: WriteFormat -> WriteFormat -> Bool # (/=) :: WriteFormat -> WriteFormat -> Bool #
Ord WriteFormat Source #
Methods compare :: WriteFormat -> WriteFormat -> Ordering # (<) :: WriteFormat -> WriteFormat -> Bool # (<=) :: WriteFormat -> WriteFormat -> Bool # (>) :: WriteFormat -> WriteFormat -> Bool # (>=) :: WriteFormat -> WriteFormat -> Bool # max :: WriteFormat -> WriteFormat -> WriteFormat # min :: WriteFormat -> WriteFormat -> WriteFormat #
Show WriteFormat Source #	Human readable names of the formats, which may include spaces or other special characters.
Methods showsPrec :: Int -> WriteFormat -> ShowS # show :: WriteFormat -> String # showList :: [WriteFormat] -> ShowS #
Convertible String WriteFormat Source #
Methods safeConvert :: String -> ConvertResult WriteFormat #
Convertible WriteFormat String Source #
Methods safeConvert :: WriteFormat -> ConvertResult String #

data WriteMode Source #

There are two writing modes currently supported:

Constructors

Pretty	pretty printing, producing a well readable, minimal ouptut
Fully	fully paranthesized printing, producing fully parenthesized expressions

Instances

Eq WriteMode Source #
Methods (==) :: WriteMode -> WriteMode -> Bool # (/=) :: WriteMode -> WriteMode -> Bool #
Ord WriteMode Source #
Methods compare :: WriteMode -> WriteMode -> Ordering # (<) :: WriteMode -> WriteMode -> Bool # (<=) :: WriteMode -> WriteMode -> Bool # (>) :: WriteMode -> WriteMode -> Bool # (>=) :: WriteMode -> WriteMode -> Bool # max :: WriteMode -> WriteMode -> WriteMode # min :: WriteMode -> WriteMode -> WriteMode #
Convertible String WriteMode Source #
Methods safeConvert :: String -> ConvertResult WriteMode #
Convertible WriteMode String Source #
Methods safeConvert :: WriteMode -> ConvertResult String #

data Semantics Source #

Semantic types.

Constructors

SemanticsMealy	Standard Mealy machine semantics.
SemanticsMoore	Standard Moore machine semantics.
SemanticsStrictMealy	Mealy machine semantics with strict envionment assumptions.
SemanticsStrictMoore	Moore machine semantics with strict envionment assumptions.

Instances

Eq Semantics Source #
Methods (==) :: Semantics -> Semantics -> Bool # (/=) :: Semantics -> Semantics -> Bool #
Ord Semantics Source #
Methods compare :: Semantics -> Semantics -> Ordering # (<) :: Semantics -> Semantics -> Bool # (<=) :: Semantics -> Semantics -> Bool # (>) :: Semantics -> Semantics -> Bool # (>=) :: Semantics -> Semantics -> Bool # max :: Semantics -> Semantics -> Semantics # min :: Semantics -> Semantics -> Semantics #
Convertible String Semantics Source #
Methods safeConvert :: String -> ConvertResult Semantics #
Convertible Semantics String Source #
Methods safeConvert :: Semantics -> ConvertResult String #

data Target Source #

Target types.

Constructors

TargetMealy	Mealy machine target
TargetMoore	Moore machine target

Instances

Eq Target Source #
Methods (==) :: Target -> Target -> Bool # (/=) :: Target -> Target -> Bool #
Ord Target Source #
Methods compare :: Target -> Target -> Ordering # (<) :: Target -> Target -> Bool # (<=) :: Target -> Target -> Bool # (>) :: Target -> Target -> Bool # (>=) :: Target -> Target -> Bool # max :: Target -> Target -> Target # min :: Target -> Target -> Target #
Convertible String Target Source #
Methods safeConvert :: String -> ConvertResult Target #
Convertible Target String Source #
Methods safeConvert :: Target -> ConvertResult String #

data Specification Source #

Internal representation of a specification.

data Error Source #

Internal representation of an error.

Instances

Show Error Source #
Methods showsPrec :: Int -> Error -> ShowS # show :: Error -> String # showList :: [Error] -> ShowS #

Configurations

defaultCfg :: Configuration Source #

inputFiles     = []
outputFile     = Nothing
outputFormat   = FULL
outputMode     = Pretty
partFile       = Nothing
busDelimiter   = "_"
primeSymbol    = "'"
atSymbol       = "@"
fromStdin      = False
owSemantics    = Nothing
owTarget       = Nothing
owParameter    = []
simplifyWeak   = False
simplifyStrong = False
negNormalForm  = False
pushGlobally   = False
pushFinally    = False
pushNext       = False
pullGlobally   = False
pullFinally    = False
pullNext       = False
noWeak         = False
noRelease      = False
noFinally      = False
noGlobally     = False
noDerived      = False
cGR            = False
check          = False
pTitle         = False
pDesc          = False
pSemantics     = False
pTarget        = False
pTags          = False
pParameters    = False
pInputs        = False
pOutputs       = False
pInfo          = False
pVersion       = False
pHelp          = False
pReadme        = False
pReadmeMd      = False
saveConfig     = []

update :: Configuration -> String -> Either Error Configuration Source #

Parses configuration parameters from the content of a configuration file and updates the respective entries in the provided configuration.

verify :: Configuration -> Either Error () Source #

Verifies that a configuration does not contain invalid parameter combinations.

Specifcations

source :: Specification -> String Source #

Returns the TSLF source of a specification.

title :: Specification -> String Source #

Returns the title of a specification.

description :: Specification -> String Source #

Returns the description of a specification.

semantics :: Specification -> Semantics Source #

Returns the semantics of a specification.

target :: Specification -> Target Source #

Returns the target flag of a specification.

tags :: Specification -> [String] Source #

Returns the tag list of a specification.

parameters :: Specification -> [String] Source #

Returns the parameters of a specification.

signals :: Configuration -> Specification -> Either Error ([String], [String]) Source #

Returns the signals of a specification using the format as implied by the given configuration.

inputs :: Configuration -> Specification -> Either Error [String] Source #

Returns the input signals of a specification using the format as implied by the given configuration.

outputs :: Configuration -> Specification -> Either Error [String] Source #

Returns the ouputs signals of a specification using the format as implied by the given configuration.

symboltable :: Specification -> String Source #

Returns the symbol table of a specification in CSV format.

fromTLSF :: String -> Either Error Specification Source #

Parses a specification in TLSF.

apply :: Configuration -> Specification -> Either Error String Source #

Applies the parameters of in the configuration and turns the given specification into the desired target format.

Fragment Detection

checkGR :: Specification -> Either Error Int Source #

Checks whether a given specification is in the Generalized Reactivity fragment. If this is the case, the reactivity level is returned. Otherwise, the check returns "-1".

Meta Information

version :: [Char] Source #

Returns the build version of the library. Requires the library to be built with cabal or stack.