search

moves-rwth / prophesy

Parameter Synthesis in Markov Models
https://moves-rwth.github.io/prophesy/
GNU General Public License v3.0
6 stars 3 forks source link

Looking for a way to combine a boolean value and a factorizedRationalFunction #6

Closed oyendrila-dobe closed 4 years ago

oyendrila-dobe commented 4 years ago

I'm trying to 'and' a boolean value with a value of datatype factorizedrationalfunction (say, p^2 + 1, where p is a parameter in my pDTMC), and store it as an expression. For eg, true & (p^2 +1). Could you give me an example of how to do it, if at all it can be done? factorizedrationalfunction doesn't seem to be used for anything other than simplerationalconstraints. Is there anyway to combine them in an single expression using and, or, or implies

sjunges commented 4 years ago

What type should have true & (p^2 + 1) have? The first is a Bool, the second a polynomial. I have never seen such an operation before.

You might want pycarl.formulae.

oyendrila-dobe commented 4 years ago

Since I'm doing a symbolic execution, there are cases where the the antecedent and precedent of an operation is coming up to this. I could not find something in the python formula part which could easily combine those two distinct types of datatypes.

sjunges commented 4 years ago

As I have never seen such a data structure and I still suspect that pycarl.formula is the right data structure (potentially after getting rid of the factorization) I do not see a way to fix this issue.

Feel free to add such data structure to prophesy using a pull request.

oyendrila-dobe commented 4 years ago

As you said, the pycarl.formula was enough to handle my issue. It's just that the FactorizedrationalFunctions have to be properly extracted and converted to Polynomials, Constraints, and finally a formula. Thanks for pointing me in the right direction.