search

gerasimou / EvoChecker

EvoChecker
GNU General Public License v2.0
4 stars 3 forks source link

Using an LTL property as a constraint doesn't work #7

Open ytzemih opened 3 years ago

ytzemih commented 3 years ago

I'd like to use properties of the kind 

// Constraint, max, 1
E [ F (A & (F B)) ]

but EvoChecker stopps enumerating solutions and creates an incomplete solution set and Pareto front.

maormann commented 3 months ago

I just stumbled across this and know I am late. EvoChecker uses PRISM v4.5, but LTL properties were only introduced with PRISM v4.7.

ytzemih commented 3 months ago

Thanks, @maormann for your response.

Generally, LTL properties were available in PRISM 4.5 and earlier. I've been using them a lot over the past years. I presume what you meant is that they could not be used directly as constraints in optimisation queries. That's I think right. However, my understanding is/was that EC does not use PRISM optimisation queries, so I was hoping to be able to use LTL that way. Anyway, I was able to solve the problem in another way.

All the best.

maormann commented 3 months ago

Hi @ytzemih, thanks for sharing your knowledge. I'm relative new to PRISM and was looking for a solution of another problem I encountered. Going trough the version history I thought it make a lot of sense. Knowing now that LTL also worked earlier makes me wish I had tried (and reproduced) it before.

However. Thanks for the response and all the best from me too.

ytzemih commented 3 months ago

No worries. Had similar problems when I first used PRISM. You need to be careful how you combine properties and models. For example, with DTMCs there is a larger fragment of CTL/LTL at your disposal than there is with MDPs. The manual does a decent job in giving a good overview of these constraints. However, I've worked closes to the limits of that tool and then your last resort are the error messages coming through.

gerasimou commented 2 months ago

@ytzemih if you could share an example or a MWE to check this, it would be great.

ytzemih commented 2 months ago

@gerasimou, thanks for getting back to me. Well, unfortunately and unsurprisingly, I don't remember, it's really a long time ago and a whole lot has happened since then. I think, I did numerous trials and, at some point, I might have sacrificed either the property or the PRISM file or I found a good alternative and it worked. I might even have excluded that part altogether from the experiment from my analysis. I didn't archive these non-working intermediate file versions, sorry.