Partial Expression Evaluation

[RileyLRoberts]

I was wondering if momba included any tools for expression evaluation? If not, could it be added? My use case is that I am attempting to create a script that applies an automated abstraction technique to jani models. I read the jani into the proper momba classes and have been able to build the abstracted model by reading the original. However, after doing some evaluations, I run into places where I have guards such as: if (2 < 3 AND x) as a guard for one statement, and then if (1< 2 AND x) as the guard for another. My tool needs to recognize these and identical guards in order to merge the two edges. So, I need a tool that would evaluate the Expression objects from momba.model down to their most simple form. I know this tool exists within the full modest toolset, as the expressions are simplified if I use Mosta (a tool in the modest toolset) to visualize the resulting automata.

Thank You,
Riley

[koehlma]

Hello Riley,

Thanks for considering Momba!

Full evaluation of expressions is already possible (for MDPs and PTAs and some other model types) as part of Momba’s explicit state space exploration engine. However, you seem to be interested in partial (or symbolical) evaluation without building the whole state space. Partial or symbolical evaluation are not currently implemented but could certainly and relatively easily be implemented and added to Momba. Do you just need to fold constants, or do you also want to apply some other, more sophisticated, simplification techniques?

I quickly threw together an example how constant folding could be done:

https://github.com/koehlma/momba/blob/main/examples/fold_constants.py

The function fold_constants successfully rewrites both expressions you provided. Some operators (e.g., the comparison operators) already come with a native_function which applies the operator to Python values. This does make constant folding much easier. In fact, these are remnants from the first state space exploration engine written in Python.

Would you be willing to invest some time in implementing these simplifications?

[RileyLRoberts]

Thanks for your response! I think the simple constant folding should work for my use case, let me try using the example code you gave and see if that is all I will need or if I need more. Were you wondering if I could fully implement the constant folding, or only other simplification techniques if I need them? I only ask because it seems you may already have a working version of the fold constants function? I am currently working towards a paper deadline in late January, but if I do end up needing to implement more than what you have already provided, and I have time, then I'm not opposed to spending a bit of time to integrate whatever I come up with into your codebase. Once again, it depends on the extent of simplification I end up needing, as what you already have may suffice.

[koehlma]

I think that constant folding and other simplifications could be useful for others as well. So, it would be great if they find their way back into Momba – if possible. This may also require some additions to the core API of Momba. My question basically was whether you would be willing to integrate the simplifications you need (and maybe more if you feel like it) back into Momba.

[RileyLRoberts]

Maximilian, I apologize for the late response. I ended up graduating and leaving this project before I got to fully investigate extending the folding to all operations. The operations you did implement worked well, but like I said I never got the time to add anything. It appears the new student on the project may be taking it a different direction, but my professor knows to reach out to you if they end up using Momba and need help. Thanks again!

…

-Riley

Sent from my iPhone

On Dec 17, 2021, at 12:37 AM, Maximilian Köhl ***@***.***> wrote:  I think that constant folding and other simplifications could be useful for others as well. So, it would be great if they find their way back into Momba – if possible. This may also require some additions to the core API of Momba. My question basically was whether you would be willing to integrate the simplifications you need (and maybe more if you feel like it) back into Momba. — Reply to this email directly, view it on GitHub, or unsubscribe. Triage notifications on the go with GitHub Mobile for iOS or Android. You are receiving this because you authored the thread.