0

I'm developing a Python framework that's used to compose logic formulas. For example, if I request mutual exclusion between a and b, the output would be the Boolean formula:

"(a --> ¬b)^(b --> ¬a)"

In addition, I want to use some formulas as building blocks for building different types of formulas, such as formulas in Linear Temporal Logic (which is a superset of Boolean logic).

The question is twofold:

  1. Do I define one base class (e.g. BooleanFormula) and then:
    • add methods for generating specific formulas (e.g. gen_mutex_formula(a, b)) ?
    • or define more classes (e.g. MutExFormula) that inherit from the fundamental class (BooleanFormula in my example) and generate the formulas in their constructors?
  2. When I want to create the new types of formulas, do I inherit from the classes in (1) and mask/override their methods or do I use multiple inheritance. Example of the latter:

    class LTLMutExFormula(LTLFormula, MutExFormula)

What are the criteria and heuristics I should be considering as I'm designing the framework?

PS1. I'm already defining the logic operators in a separate module.

PS2. Here's what I've been doing so far in terms of formulas: link to module on Github

  • 2
    "Overloading" generally refers to multiple functions with the same name but different parameters, located at the same level (which doesn't work in Python). You may be referring to "masking" a function from the parent class by defining one with the same name in the child class. – TigerhawkT3 Jul 31 '15 at 19:00
  • @TigerhawkT3 Yeah, that's what I meant, masking. I'll update the question. Thanks! – Spyros Maniatopoulos Jul 31 '15 at 19:02
  • 1
    The term used is *overriding*, not masking... – Bakuriu Jul 31 '15 at 19:05
  • @Bakuriu Just realized that as I was Googling for masking. Fixed. Thanks! – Spyros Maniatopoulos Jul 31 '15 at 19:09
  • 1
    What I'd probably do is to have the class that define the operators of the logic and then use some classmethods to build initial values and the operators. For example you could have something like `Fo.forall('x', (FO.var('x') > FO.var('y')) & FO.var('z') < FO.var('x'))` and you'd obtain the formula for `∀x(x > y ∧ z < x)`. Same for modalities of temporal logics. You can define formulas simply using functions: `def mutual_exclusive(p, q): p.implies(~q) & q.implies(~p)`. – Bakuriu Jul 31 '15 at 19:11
  • @Bakuriu I've already defined the operators in a separate module (https://github.com/LTLMoP/ReSpeC/blob/master/src/respec/ltl/ltl.py) The main motivation for my question is that many formulas have similar structure and/or the same preparatory work has to be done for them. For example, Boolean mutual exclusion and mutual exclusion with the "next" LTL operator: `"(Oa --> O(¬b))^(Ob --> O(¬a))"` – Spyros Maniatopoulos Jul 31 '15 at 19:18
  • 1
    I see that it looks like you are manipulating **strings** directly. I believe this is awful... using strings is exactly what will *not* allow you to do the manipulations you think. If you used classes and build the expression as a tree you could then walk around it and apply transformations so you could do things like `some_formula.replace('x', LTL.O('x'))` . Doing this with strings will be quite cumbersome. And you should read: [mutable default argument](http://stackoverflow.com/questions/1132941/least-astonishment-in-python-the-mutable-default-argument) – Bakuriu Jul 31 '15 at 19:30
  • @Bakuriu Thanks a lot for both pointers :-) – Spyros Maniatopoulos Jul 31 '15 at 19:31

0 Answers0