Skip to content
Snippets Groups Projects
Commit 123bbbec authored by daniel's avatar daniel
Browse files

can now have top-level conjunctions and disjunctions

parent 156d3986
No related branches found
No related tags found
No related merge requests found
...@@ -86,6 +86,8 @@ data RandConf ...@@ -86,6 +86,8 @@ data RandConf
,minDis :: Nat -- min number of disjuncts per disjunction (0 allows for Bot) ,minDis :: Nat -- min number of disjuncts per disjunction (0 allows for Bot)
,maxDis :: Nat -- max number of disjuncts per disjunction ,maxDis :: Nat -- max number of disjuncts per disjunction
,probAt :: Float -- probability of having an atom ,probAt :: Float -- probability of having an atom
,topCon :: Bool -- allow conjunctions at the top level
,topDis :: Bool -- allow disjunctions at the top level
} }
...@@ -114,19 +116,30 @@ someFormula modGen conf = go (depth conf) ...@@ -114,19 +116,30 @@ someFormula modGen conf = go (depth conf)
lits lits
= let as = [1..1+numAts conf] in [top,bot] ++ map PAt as ++ map NAt as = let as = [1..1+numAts conf] in [top,bot] ++ map PAt as ++ map NAt as
juncts junct_type r = \f ->
do n <- inRange r
junct_type <$> exactly n f
formulaOfDepth d formulaOfDepth d
= do (m,junct,r) <- oneOf [(Dia,Con,(minCon conf,maxCon conf)) = do (diabox,xxjuncts) <- oneOf [(Dia,Con `juncts` (minCon conf,maxCon conf))
,(Box,Dis,(minDis conf,maxDis conf))] ,(Box,Dis `juncts` (minDis conf,maxDis conf))]
n <- inRange r diabox <$> modGen <*> xxjuncts (go d)
m <$> modGen <*> (junct <$> exactly n (go d))
p = max 0 $ min 1 $ probAt conf p = max 0 $ min 1 $ probAt conf
go d go d
| d == 0 | d == 0
= oneOf lits = oneOf lits
| d == depth conf | d == depth conf
= formulaOfDepth (d-1) = let modal_form = formulaOfDepth (d-1)
in join $ oneOf $ concat
[ [modal_form]
, [Con `juncts` (minCon conf,maxCon conf) $ modal_form | topCon conf]
, [Dis `juncts` (minDis conf,maxDis conf) $ modal_form | topDis conf]
]
| otherwise | otherwise
= join $ fromFreqs [oneOf lits `withFreq` p = join $ fromFreqs [oneOf lits `withFreq` p
,formulaOfDepth (d-1) `withFreq` (1-p)] ,formulaOfDepth (d-1) `withFreq` (1-p)]
...@@ -252,6 +265,15 @@ randConf ...@@ -252,6 +265,15 @@ randConf
<> help "Probability of an atom occurring instead of a modality" <> help "Probability of an atom occurring instead of a modality"
<> showDefault <> showDefault
) )
<*> flag True False
( long "no-toplevel-conj"
<> help "Don't generate conjunctions at the top-level"
)
<*> flag True False
( long "no-toplevel-disj"
<> help "Don't generate disjunctions at the top-level"
)
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment