Commit 8908ed5d authored by Simon Prucker's avatar Simon Prucker
Browse files

Multimodal onestep K but nothing is satisfiable

parent 3b371362
......@@ -573,12 +573,27 @@ let mkRule_Fusion sort bs focus sl : stateExpander =
let oneStepSat_MultiModalK (u: bset list) sv =
let (sort, v) = sv in
let boxargs = bsetMap (lfGetDest1 sort) (bsetFilter v (fun lf -> (lfGetType sort lf) = AxF)) in
let reducedU = List.filter (fun bs -> bsetIsSubOrEqual boxargs bs) u in
let diamondargs = bsetMap (lfGetDest1 sort) (bsetFilter v (fun lf -> (lfGetType sort lf) = ExF)) in
let existsInU lf =
List.exists (fun bs -> bsetMem bs lf) reducedU in
let res = bsetForall diamondargs existsInU in
(*Filter for relations*)
let boxargsForRels = (*List of Tuples, where first arg is relation and second are all formulae under a box of that kind*)
let boxes = (bsetFilter v (fun lf -> (lfGetType sort lf) = AxF)) in
let boxRels = Array.to_list (bsetMap (lfGetDest2 sort) boxes) in
let getRelBoxargsTupleForOneRel rel =
rel, (bsetFilter boxes (fun r -> (lfGetDest2 sort r) = rel))
in
let res = List.map getRelBoxargsTupleForOneRel boxRels in
res
in
(*Make reduced U for each relation, thus List of tupels of relation and reduced U*)
let reducedU = List.map (fun (rel, boxargs) -> (rel, List.filter (fun bs -> bsetIsSubOrEqual boxargs bs) u)) boxargsForRels in
(*Make List of tupels of diamond formulae and their respective relation*)
let diamonds = bsetFilter v (fun lf -> (lfGetType sort lf) = ExF) in
let diaRels = Array.to_list (bsetMap (lfGetDest2 sort) diamonds) in
let diaargs = Array.to_list (bsetMap (lfGetDest1 sort) diamonds) in
let diaTuples = List.combine diaRels diaargs in
(*check if redU contains formula for every diamond per relation*)
let existsInU (rel, lf) =
List.exists (fun bs -> bsetMem bs lf) (List.assoc rel reducedU) in
let res = List.for_all existsInU diaTuples in
res
let rec oneStepGMLRec counters sort v currentU =
......
......@@ -11,8 +11,8 @@ let k_testcases onestep =
use_functor ~onestep: onestep "K" nop
[ sat "True"
; unsat "False"
; parseerror "{Fsdf"
(*; parseerror "Fsdf}" *)
(*; parseerror "{Fsdf"
; parseerror "Fsdf}" *)
; unsat "<r> True & [r] False"
; unsat "c |- <r> ~c"
; sat "c |- [r] ~c"
......@@ -56,8 +56,8 @@ let kd_testcases =
use_functor "KD" nop
[ sat "True"
; unsat "False"
; parseerror "{Fsdf"
(*; parseerror "Fsdf}" *)
(*; parseerror "{Fsdf"
; parseerror "Fsdf}" *)
; unsat "<r> True & [r] False"
; unsat "C |- <r> ~C"
; unsat "C |- [r] ~C"
......@@ -136,14 +136,13 @@ let k_onestepFunc =
use_functor ~onestep: true "K" nop
[ sat "[a1]False"
(* MULTIMODAL Tests
; unsat "[a1]False & <a2>False"
; sat "[a1]~p1 & <a2>p1"
; sat "[a1]False & <a6>p1"
; sat "[a1]False & <a2>True"
; sat "[a1]False <=> <a2>True"
; sat "[a5]False <=> <a70>True"
*)
]
let k_onestepTab =
......@@ -173,7 +172,7 @@ let k = funel_of_functor CM.MultiModalK
let prop_onestepFunc_tableau_K = onestepFunc_equals_tableau "K Property" FG.formula_K (FE.sortTableFromFunctorExp k)
let testcases =
[ (*"DL98" >::: dl98_testcases
[ "DL98" >::: dl98_testcases
; "CTL" >::: ctl_fast_testcases
; "K Tableau" >::: k_testcases false
; "K Onestep" >::: k_testcases true
......@@ -184,13 +183,15 @@ let testcases =
(*;"Nominals" >::: nominal_testcases*)
; "CL" >::: cl_testcases
; "CL" >::: cl_testcases_2agents
(* ; "PML" >::: pml_testcases (\* PML is currently disabled. *\) *)
(* ; "PML+K" >::: pmlOrK_testcases (\* PML is currently disabled. *\) *)
(* ; "PML" >::: pml_testcases (\* PML is currently disabled. *\)
; "PML+K" >::: pmlOrK_testcases (\* PML is currently disabled. *\) *)
; "K-mu (aconjunctive fragment)" >::: aconjunctive_testcases
; *)"GML" >::: gml_testcases
; "GML" >::: gml_testcases
; "Properties" >::: [prop_onestepFunc_tableau_K]
; "K onestep" >::: k_onestepFunc
; "K tableau" >::: k_onestepTab
(*
; "K onestep mulitmod" >::: k_onestepFunc
; "K tableau multimod" >::: k_onestepTab
*)
]
;;
......
......@@ -12,7 +12,7 @@ let anon_fun _ = print_endline usage_msg; raise (Exc "No anonymous arguments all
let functors = ["K"; "CL"; "GML"; "Prop"]
let matchFunctor f =
match f with
| "K" -> FG.kFormula
| "K" -> FG.kFormula ~unimodal: false
| "CL" -> FG.clFormula
| "GML" -> FG.gmlFormula
| "Prop" -> FG.propFormula
......@@ -24,7 +24,7 @@ let matchFixpoint f =
| "Mu" -> (fun x -> (U.curry (FG.formula_fp x) []))
| "CTL" -> FG.formula_ctl
| _ -> fix
let logic = ref FG.kFormula
let logic = ref (FG.kFormula ~unimodal: false)
let amount = ref 1
let size = ref 5
let fp = ref fix
......
......@@ -29,13 +29,21 @@ let propFormula formula n =
]
let relName = prefixNum "a"
let unimod_relName = return "unimod"
let boxFormula formula n = map2 (fun x y -> F.AX (x, y)) relName (formula (n-1))
let diaFormula formula n = map2 (fun x y -> F.EX (x, y)) relName (formula (n-1))
let boxFormula ?(unimodal: bool = false) formula n =
if unimodal
then map2 (fun x y -> F.AX (x, y)) unimod_relName (formula (n-1))
else map2 (fun x y -> F.AX (x, y)) relName (formula (n-1))
let kFormula formula n =
let diaFormula ?(unimodal: bool = false) formula n =
if unimodal
then map2 (fun x y -> F.EX (x, y)) unimod_relName (formula (n-1))
else map2 (fun x y -> F.EX (x, y)) relName (formula (n-1))
let kFormula ?(unimodal: bool = false) formula n =
if n > 0
then frequency [(2, propFormula formula n) ; (1, boxFormula formula n); (1, diaFormula formula n)]
then frequency [(2, propFormula formula n) ; (1, boxFormula ~unimodal: unimodal formula n); (1, diaFormula ~unimodal: unimodal formula n)]
else propFormula formula n
(*generate random subset of Agent array*)
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment