Consistent extraction of signals from a specification

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].

README.md

@@ -1,4 +1,4 @@
-# Synthesis Format Conversion Tool<br/>(Version 1.0.0.26)
+# Synthesis Format Conversion Tool<br/>(Version 1.0.0.27)
 
 A tool for reading, manipulating and transforming synthesis
 specifications in [TLSF](https://arxiv.org/abs/1604.02284).

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.

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

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
 
 -----------------------------------------------------------------------------
 

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.
 

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

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 {"

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 $
     "{" ++

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

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

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)
 
 -----------------------------------------------------------------------------
 

src/Writer/Formats/Unbeast.hs

@@ -3,9 +3,9 @@
 -- Module      :  Writer.Formats.Unbeast
 -- License     :  MIT (see the LICENSE file)
 -- Maintainer  :  Felix Klein ([email protected])
--- 
+--
 -- 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 = 
-                 "<?xml version=\"1.0\" encoding=\"ISO-8859-1\" ?>" 
+    main si so as vs =
+                 "<?xml version=\"1.0\" encoding=\"ISO-8859-1\" ?>"
       ++ "\n" ++ "<!DOCTYPE SynthesisProblem SYSTEM \""
               ++ specfile ++ "\">"
       ++ "\n"
@@ -65,18 +65,18 @@ writeFormat c s = do
       ++ "\n"
       ++ "\n" ++ "<SynthesisProblem>"
       ++ "\n" ++ "  <Title>" ++ title s ++ "</Title>"
-      ++ "\n" ++ "  <Description>" 
+      ++ "\n" ++ "  <Description>"
       ++ "\n" ++ fixedIndent (description s)
       ++ "\n" ++ "  </Description>"
       ++ "\n" ++ "  <PathToLTLCompiler>" ++ compiler
               ++ "</PathToLTLCompiler>"
       ++ "\n" ++ "  <GlobalInputs>"
       ++ concatMap printSignal si
-      ++ "\n" ++ "  </GlobalInputs>"  
+      ++ "\n" ++ "  </GlobalInputs>"
       ++ "\n" ++ "  <GlobalOutputs>"
       ++ concatMap printSignal so
       ++ "\n" ++ "  </GlobalOutputs>"
-      ++ (if null as then "" 
+      ++ (if null as then ""
           else "\n" ++ "  <Assumptions>" ++
                concatMap (\x -> "\n    <LTL>\n" ++ printFormula 6 x
                                ++ "    </LTL>\n") as ++
@@ -87,7 +87,7 @@ writeFormat c s = do
       ++ "  </Specification>"
       ++ "\n" ++ "</SynthesisProblem>"
       ++ "\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    <Bit>" ++ sig ++ "</Bit>"
 
     printFormula n f = replicate n ' ' ++ printFormula' (n + 2) f
-    
+
     printFormula' n f = case f of
       TTrue       -> "<True></True>\n"
       FFalse      -> "<False></False>\n"

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