Rename RealFunction into PseudoBooleanFunction

*Symbolic model checking for probabilistic dynamic epistemic logic*

This work consists in representing probabilistic Kripke structures by a

 symbolic representation based on Malvin Gattinger thesis[^fn1],

This work consists in representing probabilistic Kripke structures (from Probabilistic Dynamic Epistemic Logic) by a

 symbolic representation based on Malvin Gattinger thesis[^fn1] for DEL (Dynamic Epistemic Logic),

  implemented via an adapted data structure that is Albebraic Decision Diagrams (ADDs [^fn2]),

  a generalization of Binary Decision Diagrams (BDDs [^fn3]).

Team MAD at [GREYC](https://www.greyc.fr/), University of Caen Normandy, France

- sebastien.gamblin@unicaen.fr

- alexandre.niveau.unicaen.fr

- alexandre.niveau@unicaen.fr

- maroua.bouzid-mouaddib@unicaen.fr

            bot = bot.apply("+", sqsubseteq_formula(get_s(world), vocabulary, manager))

        return bot

    # v: List[str], theta: RealFunction, o: Dict[str, Formula], pi: Dict[str, Formula],

    # v: List[str], theta: PseudoBooleanFunction, o: Dict[str, Formula], pi: Dict[str, Formula],

    #                  pointed: List[str], manager, isnormalized=True, pi_in_theta=False, nb_apply=1, cache=None, **kwargs):

    proba_structure = ProbaStructure(

        vocabulary,

    pi = get_pi(event_model.probabilities, double_vocabulary_plus, manager, get_e)

    # ksv: List[str], v: List[str], theta_pre,

    #                  o: Dict[str, RealFunction], pi: Dict[str, RealFunction],

    #                  o: Dict[str, PseudoBooleanFunction], pi: Dict[str, PseudoBooleanFunction],

    #                  pointed,

    #                  manager: RealFunctionManager,

    #                  manager: PseudoBooleanFunctionManager,

    #                  v_: List[str] = [],

    #                  theta_: Dict[str, Formula] = dict(), name=None

    return ProbaTransformer(vocabulary, vocabulary_plus, conditonnal_preconditions, omega, pi, pointed, manager,

        ### This is ProbaStructure tests, for PDEL

        print(Color.get(f">FlipCoin", Color.CBOLD))

        for normalized in [False, True]:

            # Test with different type of RealFunction

            # Test with different type of PseudoBooleanFunction

            for with_probaTable in [False, True]:

                # if with_probaTable==False, ADDRealFunction

                # if with_probaTable==False, ADDPseudoBooleanFunction

                # if with_probaTable==True,  ProbaTable

                flip_coin(normalized, with_probaTable)

from src.model.datastructure.add.add_real_function import RealFunctionManager, RealFunction

from src.model.datastructure.add.add_real_function import PseudoBooleanFunctionManager, PseudoBooleanFunction

from src.model.epistemiclogic.examples.hanabi_example import *

from src.utils.timer import timeit, Timer

class SymbolicPrecondition(metaclass=ABCMeta):

    def __init__(self, manager: RealFunctionManager, vocabulary, cache: Optional[dict]=None):

    def __init__(self, manager: PseudoBooleanFunctionManager, vocabulary, cache: Optional[dict]=None):

        assert isinstance(manager, RealFunctionManager)

        assert isinstance(manager, PseudoBooleanFunctionManager)

        assert isinstance(vocabulary, list)

        self.manager = manager

class FormulaPrecondition(SymbolicPrecondition):

    def __init__(self, theta: Union[Formula, RealFunction], manager:RealFunctionManager, vocabulary: List[str], cache: Optional[dict]=None):

    def __init__(self, theta: Union[Formula, PseudoBooleanFunction], manager:PseudoBooleanFunctionManager, vocabulary: List[str], cache: Optional[dict]=None):

        assert isinstance(theta, Formula) or isinstance(theta, RealFunction)

        assert isinstance(theta, Formula) or isinstance(theta, PseudoBooleanFunction)

        super().__init__(manager, vocabulary, cache=cache)

        if isinstance(theta, Formula) and theta.isPropositionnal():

            # This pre-compilable

            self.precondition = self.manager.from_formula(theta, vars=vocabulary, cache=cache)

        elif isinstance(theta, RealFunction):

        elif isinstance(theta, PseudoBooleanFunction):

            # Nothing to do here, we have the good object

            self.precondition = theta

        else:

    filter_transformer = False

    @timeit

    def __init__(self, v: [str], theta: RealFunction, pointed: List[str], manager: RealFunctionManager, nb_apply=1, cache=None, **kwargs):

    def __init__(self, v: [str], theta: PseudoBooleanFunction, pointed: List[str], manager: PseudoBooleanFunctionManager, nb_apply=1, cache=None, **kwargs):

        """ .p65

        Common features between Knowledge Struture and Belief Structure for V, Theta, manager and pointed

        """

        assert isinstance(v, list), f"vocabulary need to be a list of str, not {type(v).__name__}"

        assert isinstance(theta, Formula) or isinstance(theta, RealFunction),  f"state_law need to be a Formula or a RealFunction, not {type(pointed).__name__}"

        assert isinstance(theta, Formula) or isinstance(theta, PseudoBooleanFunction), f"state_law need to be a Formula or a PseudoBooleanFunction, not {type(pointed).__name__}"

        assert isinstance(pointed, list), f"Pointed need to be a list of str, not {type(pointed).__name__}"

        assert isinstance(manager, RealFunctionManager), f"Manager need to be a Manager, not {type(pointed).__name__}"

        assert isinstance(manager, PseudoBooleanFunctionManager), f"Manager need to be a Manager, not {type(pointed).__name__}"

        assert isinstance(nb_apply, int), f"nb_apply need to be an int, not {type(pointed).__name__}"

        self.nb_apply = nb_apply

        return new_transformer, dico_rename_id_event, dico_rename_id_event_prime

    def update_law(self, transformer: Transformer) -> RealFunction:

    def update_law(self, transformer: Transformer) -> PseudoBooleanFunction:

        """

        - theta^new = [V_/V_°](theta /\ ||theta+||_F) /\ /\_{q \in V_} (q <-> [V_/V_°](theta_(q)))

        """

    ##################################################################

    #### definition of Translation : S5 or KD45

    @timeit

    def translation(self, phi: Formula, cache=None, show=False, **kwargs) -> RealFunction:

    def translation(self, phi: Formula, cache=None, show=False, **kwargs) -> PseudoBooleanFunction:

        """p.41

        ||T||_F = T

        ||p||_F = p

        :param ks: Structure

        :param phi: Formula

        :return: RealFunction

        :return: PseudoBooleanFunction

        """

        if cache is None: cache = {}

            assert not isinstance(form, str), f"Formula {form} need to be a formula. Not a string (Caution ? Atom(str))."

            if isinstance(form, RealFunction):

            if isinstance(form, PseudoBooleanFunction):

                #assert form.scopeEquals(self.vocabulary), \

                #    f"In left in excess (precompiled_add):{[v for v in form.getVariables() if v not in self.vocabulary]} \n" \

                #    f"In right in excess (self.vocabulary): {[v for v in self.vocabulary if v not in form.getVariables() ]}"

    @timeit

    def __init__(self, ksv: List[str], v: List[str], theta: SymbolicPrecondition,

                 pointed: List[str], manager: RealFunctionManager, v_: [str]=[], theta_: Dict[str, Formula]=dict(), name: str=None,

                 pointed: List[str], manager: PseudoBooleanFunctionManager, v_: [str]=[], theta_: Dict[str, Formula]=dict(), name: str=None,

                 precondition=None, cache=None, **kwargs):

        """

                else:

                    theta_[k] = p

                assert theta_[k].scopeEquals(self.voc_cup_voc_plus)

                assert isinstance(theta_[k], RealFunction), f"Need a ADDRealfunction or a Formula, not a {type(self.theta_[k]).__name__} with {self.theta_[k]}"

                assert isinstance(theta_[k], PseudoBooleanFunction), f"Need a ADDRealfunction or a Formula, not a {type(self.theta_[k]).__name__} with {self.theta_[k]}"

        self.theta_ = theta_

class KnowledgeStructure(Structure):

    @timeit

    def __init__(self, v: [str], theta: RealFunction, o: Dict[str, List[str]], pointed, manager, nb_apply=1, **kwargs):

    def __init__(self, v: [str], theta: PseudoBooleanFunction, o: Dict[str, List[str]], pointed, manager, nb_apply=1, **kwargs):

        """ p.39

        A tuple F = (V, theta, O)

        :param v: Finite set of atomic propositions called 'Vocabulary'

    ##################################################################

    #### definition of Translation : S5 or KD45

    @timeit

    def translation(self, phi: Formula, cache=None, show=False, **kwargs) -> RealFunction:

    def translation(self, phi: Formula, cache=None, show=False, **kwargs) -> PseudoBooleanFunction:

        """p.41

        ||Ki phi||_F = Forall(V\Oi)(theta -> ||phi||_F)

        :param ks: Structure

        :param phi: Formula

        :return: RealFunction

        :return: PseudoBooleanFunction

        """

        # print("Formula :", phi)

class BeliefStructure(Structure):

    @timeit

    def __init__(self, v: [str], theta: RealFunction, o:  Dict[str, Formula], pointed: Formula, manager: RealFunctionManager,

    def __init__(self, v: [str], theta: PseudoBooleanFunction, o:  Dict[str, Formula], pointed: Formula, manager: PseudoBooleanFunctionManager,

                 nb_apply=1, cache=None, **kwargs):

        """ p.56

        A tuple F = (V, theta, Omega)

        self.omega = {k: self.manager.from_formula(v, cache=self.cache) if isinstance(v, Formula) else v for k, v in o.items()}

        for a, oi in self.omega.items():

            assert isinstance(oi, RealFunction), f"Observations (KD45) need to be function, not : {type(oi).__name__}"

            assert isinstance(oi, PseudoBooleanFunction), f"Observations (KD45) need to be function, not : {type(oi).__name__}"

    def __repr__(self):

        res1 = Color.get(">> BeliefStructure ==\n", Color.CBOLD, Color.CGREEN2)

        return BeliefStructure(v, theta, o, self.manager, pointed)

    def translation(self, phi: Formula, cache=None, show=False, **kwargs) -> RealFunction:

    def translation(self, phi: Formula, cache=None, show=False, **kwargs) -> PseudoBooleanFunction:

        """p.30 Beyond

        [[Box_i phi||_F = Forall V' (theta' -> (Omega_i ->(||phi||_F)'))

        :param ks: Structure

        :param phi: Formula

        :return: RealFunction

        :return: PseudoBooleanFunction

        """

        assert isinstance(phi, Formula), f"Phi need to be a Formula, not a {type(phi).__name__}."

        if __debug__:

            for a, oi in self.omega.items():

                assert isinstance(oi, RealFunction), f"Observations (KD45) need to be function, not : {type(oi).__name__}"

                assert isinstance(oi, PseudoBooleanFunction), f"Observations (KD45) need to be function, not : {type(oi).__name__}"

                assert oi.scopeEquals(self.double_vocabulary_event), f"Omega scope need to be on " \

                                                                     f"{self.double_vocabulary_event} not {oi.getVariables()}."

from src.model.SMCPDEL.pySMCDEL import *

from src.model.datastructure.real_function import RealFunction

from src.model.datastructure.real_function import PseudoBooleanFunction

class ConditionalPrecondition(SymbolicPrecondition):

    def __init__(self, conditional_probabilities: Union[Dict[Formula, Tuple[Tuple[List[str], float]]], RealFunction],

                 manager: RealFunctionManager, vocabulary, vocabulary_plus, cache: dict = None):

    def __init__(self, conditional_probabilities: Union[Dict[Formula, Tuple[Tuple[List[str], float]]], PseudoBooleanFunction],

                 manager: PseudoBooleanFunctionManager, vocabulary, vocabulary_plus, cache: dict = None):

        super().__init__(manager, vocabulary, cache)

        self.vocabulary_plus = vocabulary_plus

        if isinstance(conditional_probabilities, RealFunction):

        if isinstance(conditional_probabilities, PseudoBooleanFunction):

            # Nothing to do here, we have the good object

            self.precondition = conditional_probabilities

            return

        return string

    def get_translation(self, structure: Structure) -> RealFunction:

    def get_translation(self, structure: Structure) -> PseudoBooleanFunction:

        if self.precondition is None:

            # we have a dict

            return self.__calculate_precondition(self.conditional_probabilities, structure)

class ProbaStructure(BeliefStructure):

    @timeit

    def __init__(self, v: List[str], theta: RealFunction, o: Dict[str, Formula], pi: Dict[str, Formula],

    def __init__(self, v: List[str], theta: PseudoBooleanFunction, o: Dict[str, Formula], pi: Dict[str, Formula],

                 pointed: List[str], manager, isnormalized=True, pi_in_theta=False, nb_apply=1, cache=None, **kwargs):

        super().__init__(v, theta, o, pointed, manager, nb_apply=nb_apply, cache=cache, **kwargs)

            self.pi[k] = self.manager.from_formula(pia, vars=self.double_vocabulary) if isinstance(pia, Formula) else pia

        for a, ipi in self.pi.items():

            assert isinstance(ipi, RealFunction), f"Probabilities need to be function, not : {type(ipi).__name__}"

            assert isinstance(ipi, PseudoBooleanFunction), f"Probabilities need to be function, not : {type(ipi).__name__}"

            assert ipi.scopeEquals(self.double_vocabulary), str(set(ipi.getVariables()).symmetric_difference(self.double_vocabulary))

        self.pi_in_theta = pi_in_theta

                              nb_apply=self.nb_apply, **kwargs)

    def update_law(self, transformer: Transformer) -> RealFunction:

    def update_law(self, transformer: Transformer) -> PseudoBooleanFunction:

        """

        Rewrited function to deals with Conditional Preconditions.

        - theta^new = [V_/V_°](theta /\ support(||THETA||_F)) /\ /\_{q \in V_} (q <-> [V_/V_°](theta_(q)))

    """

    @timeit

    def translation(self, phi: Formula, cache=None, show=False, **kwargs) -> RealFunction:

    def translation(self, phi: Formula, cache=None, show=False, **kwargs) -> PseudoBooleanFunction:

        if cache is None: cache = {}

    @timeit

    def __init__(self, ksv: List[str], v: List[str], theta_pre,

                 o: Dict[str, RealFunction], pi: Dict[str, RealFunction],

                 o: Dict[str, PseudoBooleanFunction], pi: Dict[str, PseudoBooleanFunction],

                 pointed,

                 manager: RealFunctionManager,

                 manager: PseudoBooleanFunctionManager,

                 v_: List[str] = [],

                 theta_: Dict[str, Formula] = dict(), name=None, precondition=None, cache=None, **kwargs):

        self.pi = {k: self.manager.from_formula(v, vars=self.double_vocabulary_event) if isinstance(v, Formula) else v for k, v in pi.items()}

        for a, ipi in self.pi.items():

            assert isinstance(ipi, RealFunction), f"Probabilities need to be function, not : {type(ipi).__name__}"

            assert isinstance(ipi, PseudoBooleanFunction), f"Probabilities need to be function, not : {type(ipi).__name__}"

            assert ipi.scopeEquals(self.double_vocabulary_event)

    def __repr__(self):