diff --git a/README b/README index a1786bc..fee74f6 100644 --- a/README +++ b/README @@ -1,5 +1,5 @@ # Synthesis Format Conversion Tool -# (Version 1.0.0.26) +# (Version 1.0.0.27) A tool for reading, manipulating and transforming synthesis specifications in TLSF [0]. diff --git a/README.md b/README.md index 6aa62d2..0671961 100644 --- a/README.md +++ b/README.md @@ -1,4 +1,4 @@ -# Synthesis Format Conversion Tool
(Version 1.0.0.26) +# Synthesis Format Conversion Tool
(Version 1.0.0.27) A tool for reading, manipulating and transforming synthesis specifications in [TLSF](https://arxiv.org/abs/1604.02284). diff --git a/src/Info.hs b/src/Info.hs index b712fdb..036cb9d 100644 --- a/src/Info.hs +++ b/src/Info.hs @@ -163,8 +163,6 @@ prInputs c s = case inputs c s of Right (x:xr) -> putStrLn $ x ++ concatMap ((:) ',' . (:) ' ') xr _ -> return () - - ----------------------------------------------------------------------------- -- | Prints the output signals of the given specification. diff --git a/src/Main.hs b/src/Main.hs index 71c1890..bffd0cc 100644 --- a/src/Main.hs +++ b/src/Main.hs @@ -26,9 +26,9 @@ import Syfco ( Configuration(..) , WriteFormat(..) , Specification + , signals , fromTLSF , apply - , partition , checkGR ) @@ -183,9 +183,13 @@ writeOutput c s = case apply c s of UNBEAST -> writeFile (rmSuffix f ++ ".xml") wc _ -> writeFile f wc - when (isJust $ partFile c) $ case partition c s of - Left err -> prError $ show err - Right f -> writeFile (fromJust $ partFile c) f + when (isJust $ partFile c) $ case signals c s of + Left err -> prError $ show err + Right (is,os) -> + writeFile (fromJust $ partFile c) $ unlines + [ ".inputs" ++ concatMap (' ' :) is + , ".outputs" ++ concatMap (' ' :) os + ] where rmSuffix path = case reverse path of diff --git a/src/Syfco.hs b/src/Syfco.hs index 735cc2f..c5a42f2 100644 --- a/src/Syfco.hs +++ b/src/Syfco.hs @@ -37,11 +37,11 @@ module Syfco , target , tags , parameters + , signals , inputs , outputs , symboltable , fromTLSF - , partition , apply -- * Fragment Detection , checkGR @@ -74,7 +74,10 @@ import Writer.Data import Writer ( WriteFormat(..) , apply - , partition + ) + +import Writer.Eval + ( signals ) import Data.Specification @@ -145,10 +148,9 @@ parameters s = inputs :: Configuration -> Specification -> Either Error [String] -inputs c s = case eval c s of - Left err -> Left err - Right (es,ss,rs,as,is,gs) -> - return $ fmlInputs $ And $ es ++ ss ++ rs ++ as ++ is ++ gs +inputs c s = case signals c s of + Left err -> Left err + Right (is,_) -> return is ----------------------------------------------------------------------------- @@ -158,10 +160,9 @@ inputs c s = case eval c s of outputs :: Configuration -> Specification -> Either Error [String] -outputs c s = case eval c s of - Left err -> Left err - Right (es,ss,rs,as,is,gs) -> - return $ fmlOutputs $ And $ es ++ ss ++ rs ++ as ++ is ++ gs +outputs c s = case signals c s of + Left err -> Left err + Right (_,os) -> return os ----------------------------------------------------------------------------- diff --git a/src/Writer.hs b/src/Writer.hs index e1f293f..908e514 100644 --- a/src/Writer.hs +++ b/src/Writer.hs @@ -21,7 +21,6 @@ module Writer ( WriteFormat(..) , apply - , partition ) where ----------------------------------------------------------------------------- @@ -50,10 +49,6 @@ import Writer.Error ( prError ) -import Writer.Eval - ( evalSignals - ) - import Writer.Formats ( WriteFormat(..) , needsLower @@ -83,22 +78,6 @@ import qualified Writer.Formats.Bosy as Bosy ----------------------------------------------------------------------------- --- | Creates the content of a partioning file from the lists --- of input and output signals. - -partition - :: Configuration -> Specification -> Either Error String - -partition c s = case evalSignals c s of - Left err -> Left err - Right (is,os) -> - return $ unlines - [ ".inputs" ++ concatMap (' ' :) is - , ".outputs" ++ concatMap (' ' :) os - ] - ------------------------------------------------------------------------------ - -- | Applies the parameters of in the configuration and turns the given -- specification into the desired target format. diff --git a/src/Writer/Eval.hs b/src/Writer/Eval.hs index 5594209..d317db8 100644 --- a/src/Writer/Eval.hs +++ b/src/Writer/Eval.hs @@ -9,13 +9,17 @@ -- ----------------------------------------------------------------------------- -{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE + + FlexibleContexts + + #-} ----------------------------------------------------------------------------- module Writer.Eval ( eval - , evalSignals + , signals ) where ----------------------------------------------------------------------------- @@ -216,10 +220,10 @@ eval eval c s = do (s', st0, xs) <- initialize c s - let signals = inputs s' ++ outputs s' + let ios = inputs s' ++ outputs s' stt <- execStateT (mapM_ staticBinding xs) st0 - (rr,sti) <- runStateT (mapM componentSignal signals) stt + (rr,sti) <- runStateT (mapM componentSignal ios) stt let (er,sr) = partitionEithers $ catMaybes rr es <- evalStateT (mapM evalLtl $ initially s') sti @@ -337,19 +341,18 @@ eval c s = do ----------------------------------------------------------------------------- +-- | Returns the signals of a specification using the format as +-- implied by the given configuration. --- | @evalSignals c s@ evaluates all signals of the given --- specification @s@ under the current configuration @c@. - -evalSignals +signals :: Configuration -> Specification -> Either Error ([String],[String]) -evalSignals c s = do +signals c s = do (s',st,xs) <- initialize c s - let signals = inputs s' ++ outputs s' + let ios = inputs s' ++ outputs s' stt <- execStateT (mapM_ staticBinding xs) st - stf <- execStateT (mapM_ componentSignal signals) stt + stf <- execStateT (mapM_ componentSignal ios) stt let is = map getId $ inputs s' os = map getId $ outputs s' @@ -367,7 +370,7 @@ evalSignals c s = do if needsLower (outputFormat c) then map toLower x else x - + getId v = case v of SDSingle (i,_) -> i SDBus (i,_) _ -> i diff --git a/src/Writer/Formats/Basic.hs b/src/Writer/Formats/Basic.hs index 43cf98e..2260997 100644 --- a/src/Writer/Formats/Basic.hs +++ b/src/Writer/Formats/Basic.hs @@ -70,7 +70,7 @@ writeFormat c s = do is' <- mapM (simplify (adjust c opConfig)) is gs' <- mapM (simplify (adjust c opConfig)) gs - (si,so) <- evalSignals c s' + (si,so) <- signals c s' return $ "INFO {" diff --git a/src/Writer/Formats/Bosy.hs b/src/Writer/Formats/Bosy.hs index 97fa3b6..a6920ef 100644 --- a/src/Writer/Formats/Bosy.hs +++ b/src/Writer/Formats/Bosy.hs @@ -72,7 +72,7 @@ writeFormat config specification = do assertions' <- mapM ((simplify (adjust config' opConfig)) . fGlobally) assertions guarantees' <- mapM (simplify (adjust config' opConfig)) guarantees - (inputs, outputs) <- evalSignals config' specification + (inputs, outputs) <- signals config' specification return $ "{" ++ diff --git a/src/Writer/Formats/Slugs.hs b/src/Writer/Formats/Slugs.hs index 15455d4..aa8c489 100644 --- a/src/Writer/Formats/Slugs.hs +++ b/src/Writer/Formats/Slugs.hs @@ -40,7 +40,7 @@ writeFormat c s = | level gr > 1 -> errNoGR1 ("in GR(" ++ show (level gr) ++ ")") "slugs" | primeSymbol c == "'" -> do - (iv,ov) <- evalSignals c s + (iv,ov) <- signals c s case find (== '\'') $ concat (iv ++ ov) of Nothing -> printSlugs gr Just _ -> @@ -61,7 +61,7 @@ writeFormat c s = [] -> ([],[]) x:_ -> x - (iv,ov) <- evalSignals c s + (iv,ov) <- signals c s return $ "[INPUT]" ++ "\n" ++ unlines iv diff --git a/src/Writer/Formats/SlugsIn.hs b/src/Writer/Formats/SlugsIn.hs index 507d40e..51402ae 100644 --- a/src/Writer/Formats/SlugsIn.hs +++ b/src/Writer/Formats/SlugsIn.hs @@ -50,7 +50,7 @@ writeFormat c s = [] -> ([],[]) x:_ -> x - (iv,ov) <- evalSignals c s + (iv,ov) <- signals c s return $ "[INPUT]" ++ "\n" ++ unlines iv diff --git a/src/Writer/Formats/Smv.hs b/src/Writer/Formats/Smv.hs index 3fa14f6..1488061 100644 --- a/src/Writer/Formats/Smv.hs +++ b/src/Writer/Formats/Smv.hs @@ -61,22 +61,22 @@ writeFormat config spec = do simplified_formula <- simplify (adjust config opConfig) formula - (input_signals, output_signals) <- evalSignals config spec + (input_signals, output_signals) <- signals config spec let - signals = (input_signals ++ output_signals) + all_signals = (input_signals ++ output_signals) - return $ main (printFormula opConfig (outputMode config) simplified_formula) signals + return $ main (printFormula opConfig (outputMode config) simplified_formula) all_signals where - main formula signals = + main formula xs = "MODULE main\n" ++ "\tVAR\n" - ++ (printSignals signals) + ++ (printSignals xs) ++ "\tLTLSPEC " ++ formula ++ "\n" - printSignals signals = case signals of + printSignals xs = case xs of [] -> "" - (signal:signals) -> "\t\t" ++ signal ++ " : boolean;\n" ++ (printSignals signals) + (x:xr) -> "\t\t" ++ x ++ " : boolean;\n" ++ (printSignals xr) ----------------------------------------------------------------------------- diff --git a/src/Writer/Formats/Unbeast.hs b/src/Writer/Formats/Unbeast.hs index 68b1a5d..612bd56 100644 --- a/src/Writer/Formats/Unbeast.hs +++ b/src/Writer/Formats/Unbeast.hs @@ -3,9 +3,9 @@ -- Module : Writer.Formats.Unbeast -- License : MIT (see the LICENSE file) -- Maintainer : Felix Klein (klein@react.uni-saarland.de) --- +-- -- Transforms a specification to the Unbeast format. --- +-- ----------------------------------------------------------------------------- module Writer.Formats.Unbeast where @@ -37,17 +37,17 @@ writeFormat c s = do _ -> filter (/= FFalse) $ es ++ map (\f -> fOr [fNot $ fAnd ss, f]) (map fGlobally rs ++ as) - + vs <- mapM (simplify' (c { noRelease = True, noWeak = True })) $ filter (/= TTrue) $ ss ++ [fGlobally $ fAnd is] ++ gs - (si,so) <- evalSignals c s + (si,so) <- signals c s return $ main si so us vs where - main si so as vs = - "" + main si so as vs = + "" ++ "\n" ++ "" ++ "\n" @@ -65,18 +65,18 @@ writeFormat c s = do ++ "\n" ++ "\n" ++ "" ++ "\n" ++ " " ++ title s ++ "" - ++ "\n" ++ " " + ++ "\n" ++ " " ++ "\n" ++ fixedIndent (description s) ++ "\n" ++ " " ++ "\n" ++ " " ++ compiler ++ "" ++ "\n" ++ " " ++ concatMap printSignal si - ++ "\n" ++ " " + ++ "\n" ++ " " ++ "\n" ++ " " ++ concatMap printSignal so ++ "\n" ++ " " - ++ (if null as then "" + ++ (if null as then "" else "\n" ++ " " ++ concatMap (\x -> "\n \n" ++ printFormula 6 x ++ " \n") as ++ @@ -87,7 +87,7 @@ writeFormat c s = do ++ " " ++ "\n" ++ "" ++ "\n" - + specfile = "SynSpec.dtd" compiler = "ltl2ba -f" @@ -113,14 +113,14 @@ writeFormat c s = do (' ':xr) -> if b then rmLeadingSpace a b xr - else rmLeadingSpace (' ':a) b xr - (x:xr) -> rmLeadingSpace (x:a) False xr - + else rmLeadingSpace (' ':a) b xr + (x:xr) -> rmLeadingSpace (x:a) False xr + printSignal sig = "\n " ++ sig ++ "" printFormula n f = replicate n ' ' ++ printFormula' (n + 2) f - + printFormula' n f = case f of TTrue -> "\n" FFalse -> "\n" diff --git a/syfco.cabal b/syfco.cabal index e38d30e..ab8375c 100644 --- a/syfco.cabal +++ b/syfco.cabal @@ -1,5 +1,5 @@ name: syfco -version: 1.0.0.26 +version: 1.0.0.27 synopsis: Synthesis Format Conversion Tool / Library description: Library and tool for reading, manipulating and transforming synthesis specifications. license: MIT