search

VerifiableRobotics / slugs

SmalL bUt Complete GROne Synthesizer
Other
37 stars 25 forks source link

How to change specification? #13

Closed layashamgah closed 8 years ago

layashamgah commented 8 years ago

To use LTLMop I need to change robot transition \varphi^{s}_{t} because I do not want it to go to some regions at some times. However these specifications are generated as default. How can I change the default speifications?

progirep commented 8 years ago

@spmaniato Can you address this question? I think that it deals with the way in which restrictions to allowed system transitions can be stated in the LTLMoP input language rather than in the slugs input language.

If I get it correctly, the author of the questions wants to add parts to the specification rather than removing the ones generated from the region graph.

spmaniato commented 8 years ago

Sure @progirep 👍

Hi @layashamgah, this is indeed a LTLMoP question. I'll answer here briefly: LTLMoP does let you add system safety requirements involving region propositions. The auto-generated formulas only describe the workspace topology. For example, you can say "if you are sensing danger then always not hallway", where hallway is some region. See grammar.pdf and some of the examples under LTLMoP/src/examples/

I'll close this issue now. If you have any further questions about specifying tasks in LTLMoP, please open a new issue at that repo: https://github.com/VerifiableRobotics/LTLMoP