Update to implement the CTL semantic on finite and infinite paths

@@ -3,28 +3,18 @@ from tl import parse, Phi
 from functools import reduce, lru_cache
 
 def fixpoint(fonction, start):
-        current = start
-        previous = None
-        while previous != current:
-            previous = current
-            current = fonction(current)
-        return current
+    current = start
+    previous = None
+    while previous != current:
+        previous = current
+        current = fonction(current)
+    return current
 
       
       
 ####################### CTL #######################
       
 class CTL_model_checker(object):
-    """
-    Object which can symbolically compute the subset of the universe where a given CTL formula is satisfied.
-    
-    Attributes :
-    - variables : the list of the variables
-    
-    Methods :
-    - check(formula) : returns the sdd representing the subset of the universe where the input formula is satisfied
-    - atom(var) : returns the sdd representing the subset of the universe where var is True
-    """
     def __init__ (self, universe, pred):
         """
         Input :
@@ -34,8 +24,6 @@ class CTL_model_checker(object):
         # TODO : mettre en cache les output de phi2sdd ?
         assert isinstance(universe, sdd), "universe must be of type sdd"
         assert isinstance(pred, shom), "pred must be of type shom"
-        
-        self.logic = "CTL"
 
         self.variables = next(iter(universe))[0].vars() # c'est tres sale mais je trouve pas d'autre solution pour l'instant
 
@@ -44,39 +32,31 @@ class CTL_model_checker(object):
         self.neg = lambda phi : self.CTL_True - phi 
         self.gfp = lambda fonction : fixpoint(fonction, self.CTL_True)
         self.lfp = lambda fonction : fixpoint(fonction, self.CTL_False)
-
+		
         self.EX = pred & universe
+        self.deadlock = self.neg(self.EX(self.CTL_True))
         self.EF = lambda phi : self.lfp(lambda Z : phi | self.EX(Z))
-        self.EG = lambda phi : self.gfp(lambda Z : phi & self.EX(Z))
+        self.EG = lambda phi : self.gfp(lambda Z : phi & (self.EX(Z) | self.deadlock))
         self.EU = lambda phi1, phi2 : self.lfp(lambda Z : phi2 | (phi1 & self.EX(Z)))
-        self.ER = lambda phi1, phi2 : self.gfp(lambda Z : phi2 & (phi1 | self.EX(Z)))
-        self.EW = lambda phi1, phi2 : self.gfp(lambda Z : phi2 | (phi1 & self.EX(Z)))
-
-        # definition of universal operators in term of fix points
-        self.AX = lambda phi : self.EX(phi) - self.EX(neg(phi))
+        self.EW = lambda phi1, phi2 : self.gfp(lambda Z : phi2 | (phi1 & (self.EX(Z) | self.deadlock)))
+        self.ER = lambda phi1, phi2 : self.gfp(lambda Z : phi2 & (phi1 | self.EX(Z) | self.deadlock))       
+        self.EM = lambda phi1, phi2 : self.lfp(lambda Z : phi2 & (phi1 | self.EX(Z)))
+		
+        self.AX = lambda phi : self.EX(self.CTL_True) & self.neg(self.EX(self.neg(phi)))
         self.AF = lambda phi : self.lfp(lambda Z : phi | self.AX(Z))
-        self.AG = lambda phi : self.gfp(lambda Z : phi & self.AX(Z))
+        self.AG = lambda phi : self.gfp(lambda Z : phi & (self.AX(Z) | self.deadlock))
         self.AU = lambda phi1, phi2 : self.lfp(lambda Z : phi2 | (phi1 & self.AX(Z)))
-        self.AR = lambda phi1, phi2 : self.gfp(lambda Z : phi2 & (phi1 | self.AX(Z)))
-        self.AW = lambda phi1, phi2 : self.gfp(lambda Z : phi2 | (phi1 & self.AX(Z)))
-
-        # redefinition of universal operators in term of negation of existential ones
-        self.AX = lambda phi : self.neg(self.EX(self.neg(phi))) # /!\ if there is no path from s, then s |= AX(phi) because there is no path that falsifies phi
-        self.AF = lambda phi : self.neg(self.EG(self.neg(phi)))
-        self.AG = lambda phi : self.neg(self.EF(self.neg(phi)))
-        self.AU = lambda phi1, phi2 : self.neg(self.EU(self.neg(phi2),self.neg(phi1) & self.neg(phi2)) | self.EG(self.neg(phi2)))
+        self.AW = lambda phi1, phi2 : self.gfp(lambda Z : phi2 | (phi1 & (self.AX(Z) | self.deadlock)))
+        self.AR = lambda phi1, phi2 : self.gfp(lambda Z : phi2 & (phi1 | self.AX(Z) | self.deadlock))
+        self.AM = lambda phi1, phi2 : self.lfp(lambda Z : phi2 & (phi1 | self.AX(Z)))
 
         self.unarymod = {"EX" : self.EX, "EF" : self.EF, "EG" : self.EG, "AX" : self.AX, "AF" : self.AF, "AG" : self.AG}
-        self.binarymod = {"EU" : self.EU, "ER" : self.ER, "EW" : self.EW, "AU" : self.AU, "AR" : self.AR, "AW" : self.AW}
+        self.binarymod = {"EU" : self.EU, "ER" : self.ER, "EW" : self.EW, "EM" : self.EM, "AU" : self.AU, "AR" : self.AR, "AW" : self.AW, "AM" : self.AM}
 
     @lru_cache(maxsize=None) # si la version de python etait 3.9 on pourrait utiliser functools.cache directement
     def atom(self, var):
         """
-        Input :
-        - var : string
         
-        Output :
-        The sdd representing the subset of the universe where var is True.
         """
         assert var in self.variables, var + " is not a variable"
         d = ddd.one()
@@ -109,17 +89,10 @@ class CTL_model_checker(object):
         elif phi.kind in self.binarymod:
             return self.binarymod[phi.kind](self._phi2sdd(phi.children[0]), self._phi2sdd(phi.children[1]))
         else:
-            raise ValueError(repr(phi) + "is not a " + self.logic + " CTL sub formula")
+            raise ValueError(repr(phi) + "is not a CTL sub formula")
 
             
     def check(self, formula):
-        """
-        Input :
-        - formula : string or tl.Phi object
-        
-        Output :
-        The sdd representing the subset of the universe where the formula is satisfied.
-        """
         assert isinstance(formula , str) or isinstance(formula , Phi), "The formula given in input must be a string or a parsed formula"
         if isinstance(formula , str):
             formula = parse(formula).ctl()
@@ -138,15 +111,14 @@ class FairCTL_model_checker(CTL_model_checker):
         - fairness is a list of CTL formulae (or sdd) to be used as fairness constraints (the fair trajectory must satisfy and[GF f for f in fairness])
         """
         super().__init__(universe, pred)
-        self.logic = "Fair CTL"
         if isinstance(fairness, list):
             pass
         elif isinstance(fairness, str) or isinstance(fairness, sdd) :
             fairness = [fairness]
         else:
-            raise TypeError("fairness must be a list or a string expressing a CTL formula")
+            raise TypeError("fairness must be a list, a string or a sdd expressing a CTL formula")
         if fairness == []:
-            print("The list of fairness constraints is empty, you should used the CTL_model_checker instead")
+            print("The list of fairness constraints is empty, you should use the CTL_model_checker instead")
 
         def fairness_preprocess(f):
             if isinstance(f, str) or isinstance(f, Phi):
@@ -158,21 +130,29 @@ class FairCTL_model_checker(CTL_model_checker):
 
         self.fairness = [fairness_preprocess(f) for f in fairness]
         
-        # see Symbolic Model Checking, McMillan 1993, section 6.4 or Symbolic model checking: 1020 states and beyond, Burch et al 1992, section 6.2
-        self.EG_fair = lambda phi : self.gfp(lambda Z : phi & self.EX(reduce(sdd.__and__ , [self.EU(Z, Z & f) for f in self.fairness], self.CTL_True)))
-        self.EG_fair_True = self.EG_fair(self.CTL_True)
-        self.EX_fair = lambda phi : self.EX(phi & self.EG_fair_True)
-        self.EF_fair = lambda phi : self.EF(phi & self.EG_fair_True)
-        self.EU_fair = lambda phi1, phi2 : self.EU(phi1, phi2 & self.EG_fair_True)
-
-        # definition of universal operators as negation of existential ones (not sure of myself here)
-        self.AX_fair = lambda phi : self.neg(self.EX_fair(self.neg(phi)))
+        self.EG_fair = lambda phi : self.gfp(lambda Z : phi & (self.deadlock | self.EX(reduce(sdd.__and__ , [self.EU(Z, Z & f) for f in self.fairness], self.CTL_True))))
+        super().__init__(self.EG_fair(self.CTL_True), pred)        
+        
+        # EX, AX, EU, EF, EM do not need to be redefined once universe = EG_fair(True)
+        self.EX_fair = self.EX
+        self.EF_fair = self.EF
+        # self.deadlock and self.CTL_true have changed since the redefinition of the universe into EG_fair(True)
+        self.EG_fair = lambda phi : self.gfp(lambda Z : phi & (self.deadlock | self.EX(reduce(sdd.__and__ , [self.EU(Z, Z & f) for f in self.fairness], self.CTL_True))))
+        self.EU_fair = self.EU
+        self.EW_fair = lambda phi1, phi2 : self.EU_fair(phi1, phi2) | self.EG_fair(phi1)
+        self.ER_fair = lambda phi1, phi2 : self.EW_fair(phi2, phi1 & phi2)
+        self.EM_fair = self.EM
+		
+        self.AX_fair = self.AX
         self.AF_fair = lambda phi : self.neg(self.EG_fair(self.neg(phi)))
         self.AG_fair = lambda phi : self.neg(self.EF_fair(self.neg(phi)))
-        self.AU_fair = lambda phi1, phi2 : self.neg(self.EU_fair(self.neg(phi2), self.neg(phi1) & self.neg(phi2)) | self.EG_fair(self.neg(phi2)))
-
+        self.AU_fair = lambda phi1, phi2 : self.neg(self.EU_fair(self.neg(phi2), self.neg(phi1) & self.neg(phi2))) & self.neg(self.EG_fair(self.neg(phi2)))
+        self.AW_fair = lambda phi1, phi2 : self.neg(self.EU_fair(self.neg(phi2), self.neg(phi1) & self.neg(phi2)))
+        self.AR_fair = lambda phi1, phi2 : self.AW_fair(phi2, phi1 & phi2)
+        self.AM_fair = lambda phi1, phi2 : self.AU_fair(phi2, phi1 & phi2)
+        
         self.unarymod = {"EX" : self.EX_fair, "EF" : self.EF_fair, "EG" : self.EG_fair, "AX" : self.AX_fair, "AF" : self.AF_fair, "AG" : self.AG_fair}
-        self.binarymod = {"EU" : self.EU_fair, "AU" : self.AU_fair}#, "ER" : ER, "EW" : EW, "AR" : AR, "AW" : AW}
+        self.binarymod = {"EU" : self.EU_fair, "ER" : self.ER_fair, "EW" : self.EW_fair, "EM" : self.EM_fair, "AU" : self.AU_fair, "AR" : self.AR_fair, "AW" : self.AW_fair, "AM" : self.AM_fair}