diff --git a/randcool/randcool.cabal b/randcool/randcool.cabal
new file mode 100644
index 0000000000000000000000000000000000000000..51ab4dece7594f98e8644bdf47bbd58403f52613
--- /dev/null
+++ b/randcool/randcool.cabal
@@ -0,0 +1,31 @@
+-- Initial cool2tatl.cabal generated by cabal init. For further
+-- documentation, see http://haskell.org/cabal/users-guide/
+
+name: randcool
+version: 0.1.0.0
+-- synopsis:
+-- description:
+license: PublicDomain
+license-file: LICENSE
+author: Daniel Gorín
+maintainer: jcpetruzza@gmail.com
+-- copyright:
+-- category:
+build-type: Simple
+-- extra-source-files:
+cabal-version: >=1.10
+
+executable randcool
+ main-is: randcool.hs
+ ghc-options: -Wall -O2
+ -- other-modules:
+ -- other-extensions:
+ build-depends: base >=4.6 && <4.7
+ ,containers
+ ,rand-vars
+ ,optparse-applicative
+ ,random
+ --,transformers
+ --,bytestring >= 0.10.2.0
+ -- hs-source-dirs:
+ default-language: Haskell2010
diff --git a/randcool/randcool.hs b/randcool/randcool.hs
new file mode 100644
index 0000000000000000000000000000000000000000..dfa9c893c850266f63faa286160c39022fa66f2b
--- /dev/null
+++ b/randcool/randcool.hs
@@ -0,0 +1,274 @@
+{-# LANGUAGE BangPatterns #-}
+module Main
+
+where
+
+import Control.Applicative
+import Control.Monad
+import Control.Monad.Random
+
+
+import Data.List
+import Data.Foldable ( for_ )
+import Data.Monoid
+import qualified Data.IntSet as I
+
+import Options.Applicative hiding ( Mod )
+
+import System.Random
+
+
+type Nat = Int -- for documentation, not enforced
+
+
+data Fm mod
+ =
+ PAt Nat
+ | NAt Nat
+ | Con [Fm mod]
+ | Dis [Fm mod]
+ | Dia mod (Fm mod)
+ | Box mod (Fm mod)
+
+class Mod mod where
+ showDia :: mod -> ShowS
+ showBox :: mod -> ShowS
+
+data K = K
+
+instance Mod K where
+ showDia _ = showString "<r>"
+ showBox _ = showString "[r]"
+
+newtype G = G Nat
+
+instance Mod G where
+ showDia (G n) = showString "{>" . shows n . showString " r}"
+ showBox (G n) = showString "{<=" . shows n . showString " r}"
+
+
+newtype CL = CL I.IntSet
+
+instance Mod CL where
+ showDia (CL ags) = showString "<{" . sepWith " " (I.toAscList ags) . showString "}>"
+ showBox (CL ags) = showString "[{" . sepWith " " (I.toAscList ags) . showString "}]"
+
+instance Mod mod => Show (Fm mod) where
+ showsPrec _ fm
+ = case fm of
+ PAt n -> showString "p" . shows n
+ NAt n -> showString "~p" . shows n
+
+ Con [] -> showString "True"
+ Con [f] -> shows f
+ Con fs -> showParen True $ sepWith " & " fs
+
+ Dis [] -> showString "False"
+ Dis [f] -> shows f
+ Dis fs -> showParen True $ sepWith " | " fs
+
+ Dia m f -> showDia m . shows f
+ Box m f -> showBox m . shows f
+
+top,bot :: Fm mod
+top = Con []
+bot = Dis []
+
+sepWith :: Show a => String -> [a] -> ShowS
+sepWith s = appEndo . mconcat . map Endo . intersperse (showString s) . map shows
+
+data RandConf
+ = RandConf {
+ depth :: Nat -- modal depth of the resulting formula
+ ,numAts :: Nat -- number of atoms
+ ,minCon :: Nat -- min number of conjuncts per conjunction (0 allows for Top)
+ ,maxCon :: Nat -- max number of conjuncts per conjunction
+ ,minDis :: Nat -- min number of disjuncts per disjunction (0 allows for Bot)
+ ,maxDis :: Nat -- max number of disjuncts per disjunction
+ ,probAt :: Float -- probability of having an atom
+ }
+
+
+-- Modality generators
+monoK :: Rand K
+monoK = pure K
+
+
+gradesBetween :: Nat -> Nat -> Rand G
+gradesBetween from to = G <$> inRange (from,to)
+
+
+
+numAgents :: Nat -> Rand CL
+numAgents n = CL <$> buildSet I.empty (n+1)
+ where
+ buildSet !acc m
+ | m <= 0 = pure acc
+ | otherwise = do heads <- rand
+ let acc' = if heads then acc else I.insert (m-1) acc
+ buildSet acc' (m-1)
+
+someFormula :: Rand mod -> RandConf -> Rand (Fm mod)
+someFormula modGen conf = go (depth conf)
+ where
+ lits
+ = let as = [1..1+numAts conf] in [top,bot] ++ map PAt as ++ map NAt as
+
+ formulaOfDepth d
+ = do (m,junct,r) <- oneOf [(Dia,Con,(minCon conf,maxCon conf))
+ ,(Box,Dis,(minDis conf,maxDis conf))]
+ n <- inRange r
+ m <$> modGen <*> (junct <$> exactly n (go d))
+
+ p = max 0 $ min 1 $ probAt conf
+
+ go d
+ | d == 0
+ = oneOf lits
+ | d == depth conf
+ = formulaOfDepth (d-1)
+ | otherwise
+ = join $ fromFreqs [oneOf lits `withFreq` p
+ ,formulaOfDepth (d-1) `withFreq` (1-p)]
+
+exactly :: Nat -> Rand a -> Rand [a]
+exactly n = sequence . take n . repeat
+
+main :: IO ()
+main
+ = do (randFormula,n,m_seed) <- execParser opts_info
+
+ for_ m_seed $ \given_seed ->
+ setStdGen (mkStdGen given_seed)
+
+ sequence_ $ take n $ repeat (putStrLn =<< pick randFormula)
+
+ where
+ opts_info
+ = info (helper <*> (infoOption "0.1" ( long "version" ) <*> opts))
+ ( fullDesc
+ -- <> progDesc "descr"
+ <> header "randcool"
+ )
+
+ opts
+ = (,,) <$> (genSel <*> randConf) <*> numFormulas <*> optional seed
+
+
+genSel :: Parser (RandConf -> Rand String)
+genSel
+ = (gen <$> selK) <|> (gen <$> selG) <|> (gen <$> selCL)
+
+ where
+ gen :: Mod mod => Rand mod -> RandConf -> Rand String
+ gen modGen conf = show <$> someFormula modGen conf
+
+ selK
+ = flag' monoK
+ ( long "monomodal-K"
+ <> short 'K'
+ <> help "Language is K with one modality"
+ )
+
+ selG
+ = flag' gradesBetween
+ ( long "monomodal-gml"
+ <> short 'G'
+ <> help "Language is GML with one modality"
+ )
+ <*>
+ option ( value 0
+ <> long "min-grade"
+ <> metavar "NUM"
+ <> help "Minimum possible grade"
+ <> showDefault
+ )
+ <*>
+ option ( value 7
+ <> long "max-grade"
+ <> metavar "NUM"
+ <> help "Maximum possible grade"
+ <> showDefault
+ )
+
+ selCL
+ = flag' numAgents
+ ( long "coalition-logic"
+ <> help "Language is Coalition Logic"
+ )
+ <*>
+ option ( value 5
+ <> long "num-agents"
+ <> short 'A'
+ <> metavar "NUM"
+ <> help "Number of agents"
+ <> showDefault
+ )
+
+randConf :: Parser RandConf
+randConf
+ = RandConf
+ <$> option ( value 3
+ <> long "modal-depth"
+ <> short 'd'
+ <> metavar "NUM"
+ <> help "Modal depth of the formulas"
+ <> showDefault
+ )
+ <*> option ( value 5
+ <> long "propositions"
+ <> short 'p'
+ <> metavar "NUM"
+ <> help "Number of proposition symbols"
+ <> showDefault
+ )
+ <*> option ( value 2
+ <> long "min-conjuncts"
+ <> metavar "NUM"
+ <> help "Minimum number of conjuncts per conjunction"
+ <> showDefault
+ )
+ <*> option ( value 10
+ <> long "max-conjuncts"
+ <> metavar "NUM"
+ <> help "Maximum number of conjuncts per conjunction"
+ <> showDefault
+ )
+ <*> option ( value 2
+ <> long "min-disjuncts"
+ <> metavar "NUM"
+ <> help "Minimum number of disjuncts per disjunction"
+ <> showDefault
+ )
+ <*> option ( value 10
+ <> long "max-disjuncts"
+ <> metavar "NUM"
+ <> help "Maximum number of disjuncts per disjunction"
+ <> showDefault
+ )
+ <*> option ( value 0.25
+ <> long "probability-atom"
+ <> metavar "[0..1]"
+ <> help "Probability of an atom occurring instead of a modality"
+ <> showDefault
+ )
+
+
+
+numFormulas :: Parser Nat
+numFormulas
+ = option ( value 1
+ <> long "num-formulas"
+ <> short 'n'
+ <> metavar "NUM"
+ <> help "Number of formulas to generate"
+ <> showDefault
+ )
+
+seed :: Parser Int
+seed
+ = option ( long "seed"
+ <> metavar "NUM"
+ <> help "Random seed"
+ )
+