diff --git a/hylolib.cabal b/hylolib.cabal
--- a/hylolib.cabal
+++ b/hylolib.cabal
@@ -1,5 +1,5 @@
 Name:                hylolib
-Version:             1.3.1
+Version:             1.3.2
 Synopsis:            Tools for hybrid logics related programs
 License:             GPL
 License-file:        LICENSE
@@ -15,7 +15,7 @@
   Build-Depends:       base >= 4, base < 5,
                        containers < 1,
                        array < 1,
-                       mtl >= 1, mtl < 2,
+                       mtl >= 2, mtl < 3,
                        pretty >= 1, pretty < 2,
                        random >= 1, random < 2,
                        QuickCheck >= 1, QuickCheck < 2,
diff --git a/src/HyLo/Formula/Rewrite.hs b/src/HyLo/Formula/Rewrite.hs
--- a/src/HyLo/Formula/Rewrite.hs
+++ b/src/HyLo/Formula/Rewrite.hs
@@ -29,7 +29,7 @@
 
 instance Read prop => Read (Rewr prop) where
     readPrec = RP.choice [do 'O' <- RP.get; Orig `liftM` readPrec,
-                          do RP.lift (string "RW_"); Rewr `liftM` readPrec]
+                          do _ <- RP.lift (string "RW_"); Rewr `liftM` readPrec]
 
 wrapProps :: Formula n p r -> Formula n (Rewr p) r
 wrapProps = mapSig id Orig id
diff --git a/src/HyLo/Model.hs b/src/HyLo/Model.hs
--- a/src/HyLo/Model.hs
+++ b/src/HyLo/Model.hs
@@ -85,12 +85,12 @@
 
 instance (Read w, Read n, Read p, Read r, Ord w, Ord n, Ord p, Ord r)
       => Read (Model w n p r) where
-    readPrec = do s "Model{\n"
-                  s " worlds = "; ws <- readPrec; fsep
-                  s " succs  = "; rs <- readPrec; fsep
-                  s " valP   = "; ps <- readPrec; fsep
-                  s " valN   = "; ns <- readPrec; fsep
-                  s " sig    = "; si <- readPrec; s "}"
+    readPrec = do _ <- s "Model{\n"
+                  _ <- s " worlds = "; ws <- readPrec; _ <- fsep
+                  _ <- s " succs  = "; rs <- readPrec; _ <- fsep
+                  _ <- s " valP   = "; ps <- readPrec; _ <- fsep
+                  _ <- s " valN   = "; ns <- readPrec; _ <- fsep
+                  _ <- s " sig    = "; si <- readPrec; _ <- s "}"
                   return $ model ws
                                  (rs :: [(w,r,w)])
                                  (Map.fromList ps :: Map p (Set w))
diff --git a/src/HyLo/Model/PrettyPrint.hs b/src/HyLo/Model/PrettyPrint.hs
--- a/src/HyLo/Model/PrettyPrint.hs
+++ b/src/HyLo/Model/PrettyPrint.hs
@@ -1,4 +1,4 @@
-module HyLo.Model.PrettyPrint ( toDot )
+module HyLo.Model.PrettyPrint ( toDot, toDotStr )
 
 where
 
@@ -8,7 +8,41 @@
 
 import HyLo.Model     ( Model, worlds, succs, namesOf, propsOf )
 import HyLo.Signature ( getSignature, relSymbols )
+import HyLo.Signature.String ( NomSymbol(..), PropSymbol(..), RelSymbol(..))
 
+
+toDotStr :: Model NomSymbol NomSymbol PropSymbol RelSymbol -> String
+toDotStr m = render dotDoc
+    where dotDoc  = text "digraph M" <+> lbrace $+$ (nest 2 $ vcat [
+                          text "node [fontname=helvetica];",
+                          (vcat $ map nodeDef ws),
+                          empty,
+                          text "edge [fontname=helvetica];",
+                          (vcat [relDef w r v | r <- rs,
+                                                w <- ws,
+                                                v <- toList $ succs m r w])]
+                      ) $+$
+                    rbrace
+          nodeDef w = textSN w <+> (brackets $
+                        text "label = " <>
+                         (doubleQuotes $
+                            (braces . hsep . punctuate comma $ map textSN $ namesOf w m) <> text "\\n" <>
+                            (braces . hsep . punctuate comma $ map textSP $ propsOf w m)    )) <>
+                      semi
+          relDef w r v = textSN w <+> text "->" <+> textSN v <+>
+                         labIfNeeded r <> semi
+          labIfNeeded  = if gt1 rs
+                          then \r -> brackets $
+                                 text "label =" <> doubleQuotes (textSR r)
+                          else const empty
+          --
+          ws = toList . worlds $ m
+          rs = toList . relSymbols . getSignature $ m
+          --
+          gt1 (_:_:_) = True
+          gt1 _       = False
+
+
 toDot :: (Show w, Show n, Show p, Show r, Ord w) => Model w n p r -> String
 toDot m = render dotDoc
     where dotDoc  = text "digraph M" <+> lbrace $+$ (nest 2 $ vcat [
@@ -44,3 +78,13 @@
 
 textS :: Show a => a -> Doc
 textS = text . show
+
+textSN :: NomSymbol -> Doc
+textSN (NomSymbol str) = text str
+
+textSP :: PropSymbol -> Doc
+textSP (PropSymbol str) = text str
+
+textSR :: RelSymbol -> Doc
+textSR (RelSymbol str) = text str
+textSR (InvRelSymbol str) = text ('-':str)
diff --git a/src/HyLo/Test.hs b/src/HyLo/Test.hs
--- a/src/HyLo/Test.hs
+++ b/src/HyLo/Test.hs
@@ -56,7 +56,7 @@
 mycheck :: Testable a => Config -> a -> TestCase
 mycheck config a testName align =
   do rnd <- newStdGen
-     printf "  %s" $ take (align + 10) (testName ++ repeat '.')
+     putStr ("  " ++ take (align + 10) (testName ++ repeat '.'))
      tests config (evaluate a) rnd 0 0 align []
 
 tests :: Config