Project

General

Profile

Statistics
| Branch: | Revision:

cool / randcool / randcool.hs @ 2be59dcf

History | View | Annotate | Download (7.57 KB)

1
{-# LANGUAGE BangPatterns #-}
2
module Main
3

    
4
where
5

    
6
import Control.Applicative
7
import Control.Monad
8
import Control.Monad.Random
9

    
10

    
11
import Data.List
12
import Data.Foldable ( for_ )
13
import Data.Monoid
14
import qualified Data.IntSet as I
15

    
16
import Options.Applicative hiding ( Mod )
17

    
18
import System.Random
19

    
20

    
21
type Nat = Int  -- for documentation, not enforced
22

    
23

    
24
data Fm mod
25
 =
26
   PAt  Nat
27
 | NAt  Nat
28
 | Con  [Fm mod]
29
 | Dis  [Fm mod]
30
 | Dia  mod (Fm mod)
31
 | Box  mod (Fm mod)
32

    
33
class Mod mod where
34
  showDia :: mod -> ShowS
35
  showBox :: mod -> ShowS
36

    
37
data K = K
38

    
39
instance Mod K where
40
  showDia _ = showString "<r>"
41
  showBox _ = showString "[r]"
42

    
43
newtype G = G Nat
44

    
45
instance Mod G where
46
  showDia (G n) = showString "{>"  . shows n . showString " r}"
47
  showBox (G n) = showString "{<=" . shows n . showString " r}"
48

    
49

    
50
newtype CL = CL I.IntSet
51

    
52
instance Mod CL where
53
  showDia (CL ags) = showString "<{" . sepWith " " (I.toAscList ags) . showString "}>"
54
  showBox (CL ags) = showString "[{" . sepWith " " (I.toAscList ags) . showString "}]"
55

    
56
instance Mod mod => Show (Fm mod) where
57
  showsPrec _ fm
58
   = case fm of
59
       PAt n    -> showString  "p" . shows n
60
       NAt n    -> showString "~p" . shows n
61

    
62
       Con []   -> showString "True"
63
       Con [f]  -> shows f
64
       Con fs   -> showParen True $ sepWith " & " fs
65

    
66
       Dis []   -> showString "False"
67
       Dis [f]  -> shows f
68
       Dis fs   -> showParen True $ sepWith " | " fs
69

    
70
       Dia m f -> showDia m . shows f
71
       Box m f -> showBox m . shows f
72

    
73
top,bot :: Fm mod
74
top = Con []
75
bot = Dis []
76

    
77
sepWith :: Show a => String -> [a] -> ShowS
78
sepWith s = appEndo . mconcat . map Endo . intersperse (showString s) . map shows
79

    
80
data RandConf
81
 = RandConf {
82
    depth  :: Nat      -- modal depth of the resulting formula
83
   ,numAts :: Nat      -- number of atoms
84
   ,minCon :: Nat      -- min number of conjuncts per conjunction (0 allows for Top)
85
   ,maxCon :: Nat      -- max number of conjuncts per conjunction
86
   ,minDis :: Nat      -- min number of disjuncts per disjunction (0 allows for Bot)
87
   ,maxDis :: Nat      -- max number of disjuncts per disjunction
88
   ,probAt :: Float    -- probability of having an atom
89
   ,topCon :: Bool     -- allow conjunctions at the top level
90
   ,topDis :: Bool     -- allow disjunctions at the top level
91
   }
92

    
93

    
94
-- Modality generators
95
monoK :: Rand K
96
monoK = pure K
97

    
98

    
99
gradesBetween :: Nat -> Nat -> Rand G
100
gradesBetween from to = G <$> inRange (from,to)
101

    
102

    
103

    
104
numAgents :: Nat -> Rand CL
105
numAgents n = CL <$> buildSet I.empty n
106
  where
107
    buildSet !acc m
108
      | m <= 0    = pure acc
109
      | otherwise = do heads <- rand
110
                       let acc' = if heads then acc else I.insert m acc
111
                       buildSet acc' (m-1)
112

    
113
someFormula :: Rand mod -> RandConf -> Rand (Fm mod)
114
someFormula modGen conf = go (depth conf)
115
  where
116
    lits
117
     = let as = [1..1+numAts conf] in [top,bot] ++ map PAt as ++ map NAt as
118

    
119
    juncts junct_type r = \f ->
120
       do n <- inRange r
121
          junct_type <$> exactly n f
122

    
123
    formulaOfDepth d
124
     = do (diabox,xxjuncts) <- oneOf [(Dia,Con `juncts` (minCon conf,maxCon conf))
125
                                     ,(Box,Dis `juncts` (minDis conf,maxDis conf))]
126
          diabox <$> modGen <*> xxjuncts (go d)
127

    
128

    
129
    p = max 0 $ min 1 $ probAt conf
130

    
131
    go d
132
     | d == 0
133
      = oneOf lits
134

    
135
     | d == depth conf
136
      = let modal_form = formulaOfDepth (d-1)
137
        in join $ oneOf $ concat
138
            [ [modal_form]
139
            , [Con `juncts` (minCon conf,maxCon conf) $ modal_form | topCon conf]
140
            , [Dis `juncts` (minDis conf,maxDis conf) $ modal_form | topDis conf]
141
            ]
142

    
143
     | otherwise
144
      = join $ fromFreqs [oneOf lits           `withFreq`    p
145
                         ,formulaOfDepth (d-1) `withFreq` (1-p)]
146

    
147
exactly :: Nat -> Rand a -> Rand [a]
148
exactly n = sequence . take n . repeat
149

    
150
main :: IO ()
151
main
152
 = do (randFormula,n,m_seed) <- execParser opts_info
153

    
154
      for_ m_seed $ \given_seed ->
155
        setStdGen (mkStdGen given_seed)
156

    
157
      sequence_ $ take n $ repeat (putStrLn =<< pick randFormula)
158

    
159
 where
160
  opts_info
161
   = info (helper <*> (infoOption "0.1" ( long "version" ) <*> opts))
162
            ( fullDesc
163
         -- <> progDesc "descr"
164
            <> header "randcool"
165
            )
166

    
167
  opts
168
   = (,,) <$> (genSel <*> randConf) <*> numFormulas <*> optional seed
169

    
170

    
171
genSel :: Parser (RandConf -> Rand String)
172
genSel
173
 = (gen <$> selK) <|> (gen <$> selG) <|> (gen <$> selCL)
174

    
175
 where
176
  gen :: Mod mod => Rand mod -> RandConf -> Rand String
177
  gen modGen conf = show <$> someFormula modGen conf
178

    
179
  selK
180
   = flag' monoK
181
       (  long "monomodal-K"
182
       <> short 'K'
183
       <> help "Language is K with one modality"
184
       )
185

    
186
  selG
187
   = flag' gradesBetween
188
       (  long "monomodal-gml"
189
       <> short 'G'
190
       <> help "Language is GML with one modality"
191
       )
192
     <*>
193
     option (  value 0
194
            <> long "min-grade"
195
            <> metavar "NUM"
196
            <> help "Minimum possible grade"
197
            <> showDefault
198
            )
199
     <*>
200
     option (  value 7
201
            <> long "max-grade"
202
            <> metavar "NUM"
203
            <> help "Maximum possible grade"
204
            <> showDefault
205
            )
206

    
207
  selCL
208
   = flag' numAgents
209
       (  long "coalition-logic"
210
       <> help "Language is Coalition Logic"
211
       )
212
     <*>
213
     option (  value 5
214
            <> long "num-agents"
215
            <> short 'A'
216
            <> metavar "NUM"
217
            <> help "Number of agents"
218
            <> showDefault
219
            )
220

    
221
randConf :: Parser RandConf
222
randConf
223
 = RandConf
224
    <$> option (  value 3
225
               <> long "modal-depth"
226
               <> short 'd'
227
               <> metavar "NUM"
228
               <> help "Modal depth of the formulas"
229
               <> showDefault
230
               )
231
    <*> option (  value 5
232
               <> long "propositions"
233
               <> short 'p'
234
               <> metavar "NUM"
235
               <> help "Number of proposition symbols"
236
               <> showDefault
237
               )
238
    <*> option (  value 2
239
               <> long "min-conjuncts"
240
               <> metavar "NUM"
241
               <> help "Minimum number of conjuncts per conjunction"
242
               <> showDefault
243
               )
244
    <*> option (  value 10
245
               <> long "max-conjuncts"
246
               <> metavar "NUM"
247
               <> help "Maximum number of conjuncts per conjunction"
248
               <> showDefault
249
               )
250
    <*> option (  value 2
251
               <> long "min-disjuncts"
252
               <> metavar "NUM"
253
               <> help "Minimum number of disjuncts per disjunction"
254
               <> showDefault
255
               )
256
    <*> option (  value 10
257
               <> long "max-disjuncts"
258
               <> metavar "NUM"
259
               <> help "Maximum number of disjuncts per disjunction"
260
               <> showDefault
261
               )
262
    <*> option ( value 0.25
263
              <> long "probability-atom"
264
              <> metavar "[0..1]"
265
              <> help "Probability of an atom occurring instead of a modality"
266
              <> showDefault
267
              )
268
    <*> flag True False
269
              (  long "no-toplevel-conj"
270
              <> help "Don't generate conjunctions at the top-level"
271
              )
272
    <*> flag True False
273
              (  long "no-toplevel-disj"
274
              <> help "Don't generate disjunctions at the top-level"
275
              )
276

    
277

    
278

    
279

    
280
numFormulas :: Parser Nat
281
numFormulas
282
 = option (  value 1
283
          <> long "num-formulas"
284
          <> short 'n'
285
          <> metavar "NUM"
286
          <> help "Number of formulas to generate"
287
          <> showDefault
288
          )
289

    
290
seed :: Parser Int
291
seed
292
 = option (  long "seed"
293
          <> metavar "NUM"
294
          <> help "Random seed"
295
          )
296