Add timeout.

mc_openapi/doml_mc/imc.py

@@ -142,9 +142,10 @@ class IntermediateModelChecker:
         self.intermediate_model = intermediate_model
         instantiate_solver()
 
-    def check_requirements(self, reqs: RequirementStore) -> MCResults:
-        results = []
+    def check_requirements(self, reqs: RequirementStore, timeout: int = 0) -> MCResults:
+        self.solver.set(timeout=(timeout * 1000))
 
+        results = []
         for req in reqs.get_all_requirements():
             self.solver.push()
             self.solver.assert_and_track(

mc_openapi/doml_mc/mc.py

@@ -2,6 +2,7 @@ from typing import Optional
 import importlib.resources as ilres
 import yaml
 from joblib import parallel_backend, Parallel, delayed
+from multiprocessing import TimeoutError
 
 from .. import assets
 from .intermediate_model.doml_element import (
@@ -14,7 +15,7 @@ from .intermediate_model.metamodel import (
     parse_metamodel
 )
 from .xmi_parser.doml_model import parse_doml_model
-from .mc_result import MCResults
+from .mc_result import MCResult, MCResults
 from .imc import RequirementStore, IntermediateModelChecker
 from .common_reqs import CommonRequirements
 from .consistency_reqs import (
@@ -41,7 +42,7 @@ class ModelChecker:
         self.intermediate_model: IntermediateModel = parse_doml_model(xmi_model, ModelChecker.metamodel)
         reciprocate_inverse_associations(self.intermediate_model, ModelChecker.inv_assoc)
 
-    def check_common_requirements(self, threads=1, consistency_checks=False) -> MCResults:
+    def check_common_requirements(self, threads: int = 1, consistency_checks: bool = False, timeout: Optional[int] = None) -> MCResults:
         assert ModelChecker.metamodel and ModelChecker.inv_assoc
         req_store = CommonRequirements
         if consistency_checks:
@@ -59,7 +60,7 @@ class ModelChecker:
 
         if threads <= 1:
             imc = IntermediateModelChecker(ModelChecker.metamodel, ModelChecker.inv_assoc, self.intermediate_model)
-            reqs = imc.check_requirements(req_store)
+            reqs = imc.check_requirements(req_store, timeout=(0 if timeout is None else timeout))
             return reqs
         else:
             def split_reqs(n_reqs: int, n_split: int):
@@ -70,9 +71,12 @@ class ModelChecker:
                     rto = min(rfrom + slice_size, n_reqs)
                     yield rfrom, rto
 
+            try:
                 with parallel_backend('threading', n_jobs=threads):
-                results = Parallel()(delayed(worker)(rfrom, rto) for rfrom, rto in split_reqs(len(req_store), threads))
+                    results = Parallel(timeout=timeout)(delayed(worker)(rfrom, rto) for rfrom, rto in split_reqs(len(req_store), threads))
                 ret = MCResults([])
                 for res in results:
                     ret.add_results(res)
                 return ret
+            except TimeoutError:
+                return MCResults([(MCResult.dontknow, "")])

mc_openapi/doml_mc/mc_result.py

@@ -25,7 +25,7 @@ class MCResult(Enum):
 
 
 class MCResults:
-    dontknow_msg = "Unable to check some requirements."
+    dontknow_msg = "Timed out: unable to check some requirements."
 
     def __init__(self, results: list[tuple[MCResult, str]]):
         self.results = results

mc_openapi/doml_mc/test.ipynb

@@ -23,7 +23,7 @@
    "metadata": {},
    "outputs": [],
    "source": [
-    "r = dmc.check_common_requirements(2)\n",
+    "r = dmc.check_common_requirements(2, False, 50)\n",
     "r.summarize()"
    ]
   }

mc_openapi/handlers.py

@@ -13,7 +13,7 @@ def post(body, requirement=None):
     doml_xmi = body
     try:
         dmc = ModelChecker(doml_xmi)
-        results = dmc.check_common_requirements(2)
+        results = dmc.check_common_requirements(threads=2, consistency_checks=False, timeout=50)
         res, msg = results.summarize()
 
         if res == MCResult.sat: