GML multimodal with bugs

lib/src/CoAlgLogics.ml

@@ -589,38 +589,53 @@ let rec oneStepGMLRec counters sort v currentU =
     then false
   else
   let filterUnsatDiamond lf = 
-     ((lfGetType sort lf = MoreThanF) && ((lfGetDestNum sort lf) >= (Hashtbl.find counters lf))) in
+      ((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 filterCoreLabels bset = 
+  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 = 
     bsetExists filteredV (fun lf -> bsetMem bset (lfGetDest1 sort lf)) in
-  let filteredU = List.filter filterCoreLabels currentU in
-  if filteredU = [] then false
+  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
   else
-  let u = List.hd filteredU in
-  let updateCountersAdd lf = 
-    let modalArg = lfGetDest1 sort lf in
-    let newVal = (Hashtbl.find counters lf) + 1 in
-    match lfGetType sort lf with
-    | MoreThanF -> if bsetMem u modalArg then Hashtbl.add counters lf newVal
-    | MaxExceptF -> if not (bsetMem u modalArg) then Hashtbl.add counters lf newVal
-    | _ -> ()
-  in
-  let updateCountersRem lf = 
-    let modalArg = lfGetDest1 sort lf in
-    match lfGetType sort lf with
-    | MoreThanF -> if bsetMem u modalArg then Hashtbl.remove counters lf
-    | MaxExceptF -> if not (bsetMem u modalArg) then Hashtbl.remove counters lf
-    | _ -> ()
+  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
+      let newVal = (Hashtbl.find counters lf) + 1 in
+      match lfGetType sort lf with
+      | MoreThanF -> bsetMem u modalArg then Hashtbl.add counters lf newVal
+      | MaxExceptF -> not (bsetMem u modalArg) then Hashtbl.add counters lf newVal
+      | _ -> ()
+    in
+    let updateCountersRem lf = 
+      let modalArg = lfGetDest1 sort lf in
+      match lfGetType sort lf with
+      | MoreThanF -> bsetMem u modalArg then Hashtbl.remove counters lf
+      | MaxExceptF -> not (bsetMem u modalArg) then Hashtbl.remove counters lf
+      | _ -> ()
+    in
+    let fitleredV = (List.assoc rel filteredVsForRels) in
+    bsetIter updateCountersAdd filteredV;
+    if ((oneStepGMLRec counters sort filteredV filteredU)) then true
+    else begin
+      bsetIter updateCountersRem filteredV;
+      if (oneStepGMLRec counters sort filteredV (List.tl filteredU)) then true
+      else false
+    end
   in
-  bsetIter updateCountersAdd v;
-  if ((oneStepGMLRec counters sort v filteredU)) then true
-  else begin
-    bsetIter updateCountersRem v;
-    if (oneStepGMLRec counters sort v (List.tl filteredU)) then true
-    else false
-  end
+  List.fold_left handleRel true filteredUsForRels
 
 let rec oneStepGMLRec2 currentA sort v u =
   let boxLimitReached lf = 
@@ -660,6 +675,8 @@ let oneStepSat_GML u sv =
   let counters = Hashtbl.create (bsetLen v) in
   bsetIter (fun lf -> Hashtbl.add counters lf 0) v;
   oneStepGMLRec counters sort v u
+                    
+  
 
 
 let implementationLookup = [ (MultiModalK, These (mkRule_MultiModalK, oneStepSat_MultiModalK))