Unverified Commit 01cf0e5b authored by Merlin's avatar Merlin 💧
Browse files

Fixed multimodal GML?

parent 702f9714
Pipeline #14951 waiting for manual action with stages
......@@ -583,33 +583,19 @@ let oneStepSat_MultiModalK (u: bset list) sv =
bsetForall diamonds (fun lf -> existsInU (lfGetDest3 sort lf) (lfGetDest1 sort lf))
let rec oneStepGMLRec counters sort v currentU =
let isExceedingBox lf =
(lfGetType sort lf = MaxExceptF) && ((lfGetDestNum sort lf) < (Hashtbl.find counters lf)) in
let isExceedingBox lf = (lfGetType sort lf = MaxExceptF) && ((lfGetDestNum sort lf) < (Hashtbl.find counters lf)) in
if (bsetExists v isExceedingBox)
then false
else
let filterUnsatDiamond lf =
((lfGetType sort lf = MoreThanF) && ((lfGetDestNum sort lf) >= (Hashtbl.find counters lf))) in
let filterUnsatDiamond lf = (lfGetType sort lf = MoreThanF) && ((lfGetDestNum sort lf) >= (Hashtbl.find counters lf)) in
let filteredV = bsetFilter v filterUnsatDiamond in
if (bsetIsSubOrEqual filteredV (bsetMake())) then true
else
let neededRels =
let neededRelsDuplicates = bsetMap (lfGetDest3 sort) filteredV in
let elimDups result elem =
if List.mem elem result
then result
else elem :: result
in
Array.fold_left elimDups [] neededRelsDuplicates in
let filteredVsForRels =
List.map (fun rel -> (rel, (bsetFilter filteredV (fun lf -> (lfGetDest3 sort lf) = rel)))) neededRels in
let filterCoreLabels filteredV bset =
let filterCoreLabels bset =
bsetExists filteredV (fun lf -> bsetMem bset (lfGetDest1 sort lf)) in
let filteredUsForRels = List.map (fun (rel, filteredV) -> (rel, List.filter (filterCoreLabels filteredV) currentU)) filteredVsForRels in
if List.exists (fun (rel, l) -> l = []) filteredUsForRels then false
let filteredU = List.filter filterCoreLabels currentU in
if filteredU = [] then false (* ensures early termination and guards the List.hd below *)
else
let handleRel satisfiable (rel, filteredU) =
if satisfiable = false then false else
let u = List.hd filteredU in
let updateCountersAdd lf =
let modalArg = lfGetDest1 sort lf in
......@@ -626,55 +612,24 @@ let rec oneStepGMLRec counters sort v currentU =
| MaxExceptF -> if not (bsetMem u modalArg) then Hashtbl.remove counters lf
| _ -> ()
in
let filteredV = (List.assoc rel filteredVsForRels) in
bsetIter updateCountersAdd filteredV;
if ((oneStepGMLRec counters sort filteredV filteredU)) then true
bsetIter updateCountersAdd v;
if ((oneStepGMLRec counters sort v filteredU)) then true
else begin
bsetIter updateCountersRem filteredV;
if (oneStepGMLRec counters sort filteredV (List.tl filteredU)) then true
bsetIter updateCountersRem v;
if (oneStepGMLRec counters sort v (List.tl filteredU)) then true
else false
end
in
List.fold_left handleRel true filteredUsForRels
let rec oneStepGMLRec2 currentA sort v u =
let boxLimitReached lf =
let m = lfGetDestNum sort lf in
let arg = lfGetDest1 sort lf in
let countBoxes res a =
if not (bsetMem a arg) then res + 1 else res in
List.fold_left countBoxes 0 currentA > m in
let boxes = bsetFilter v (fun lf -> lfGetType sort lf = MaxExceptF) in
if (bsetExists boxes boxLimitReached) then false
else begin
let diamondNotSat lf =
let m = lfGetDestNum sort lf in
let arg = lfGetDest1 sort lf in
let countDiamonds res a =
if bsetMem a arg then res + 1 else res in
List.fold_left countDiamonds 0 currentA <= m in
let diamonds = bsetFilter v (fun lf -> (lfGetType sort lf = MoreThanF) && (diamondNotSat lf)) in
if (bsetIsSubOrEqual diamonds (bsetMake())) then true
else begin
let filterCoreLabels bset =
bsetExists diamonds (fun lf -> (lfGetType sort lf = MoreThanF) && (bsetMem bset (lfGetDest1 sort lf))) in
let filteredU = List.filter filterCoreLabels u in
if filteredU = [] then false
else begin
let aToAdd = List.hd filteredU in
let remainingU = List.tl filteredU in
(oneStepGMLRec2 currentA sort v remainingU) || (oneStepGMLRec2 (aToAdd::currentA) sort v filteredU)
end
end
end
let oneStepSat_GML u sv =
let (sort, v) = sv in
let counters = Hashtbl.create (bsetLen v) in
bsetIter (fun lf -> Hashtbl.add counters lf 0) v;
oneStepGMLRec counters sort v u
let rels = bsetFold (fun lf accu -> let role = lfGetDest3 sort lf in role :: accu) v [] in
let reled_v = List.map (fun rel -> (rel, bsetFilter v (fun lf -> lfGetDest3 sort lf = rel))) rels in
List.for_all (fun (rel, sub_v) ->
let counters = Hashtbl.create (bsetLen sub_v) in
bsetIter (fun lf -> Hashtbl.add counters lf 0) v;
oneStepGMLRec counters sort sub_v u
) reled_v
......
......@@ -115,8 +115,9 @@ let gml_testcases =
use_functor ~onestep: true "GML" nop
[ unsat "(<8>(P & ~Q)) & (<8>(Q & ~P)) & ([17](P & Q))"
; sat "<9 a1><7 a1>p3 | (<7 a1>p7 <=> True <=> p2)"
; unsat "<10 a1>([8 a1]True | [7 a1]p8 <=> [0 a1]p3 & ~True)"
; unsat "<3 a1>~p & [0 a1]p"
; unsat "<10 a1>([8 a1]True | [7 a1]p8 <=> [0 a1]p3 & ~True)"
; unsat "<3 a1>~p & [0 a1]p"
; sat "<3 a1>~p & [0 a2]p"
]
let pml_testcases =
......
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