search

VerifiableRobotics / LTLMoP

A toolkit for designing and implementing LTL-based task specifications.
http://ltlmop.github.io
GNU General Public License v3.0
56 stars 70 forks source link

Analyze shows slurptest.spec as unrealizable #11

Closed ConstantineLignos closed 12 years ago

ConstantineLignos commented 12 years ago

Reproduction steps:

  1. Checkout latest slurp-dev (cc96ed4).
  2. Run python specEditor.py examples/slurptest/slurptest.spec
  3. Debug --> Analyze (you can compile first, it doesn't matter)

Expected: Analysis window shows that the spec is okay. Actual: See "System highlighted goal(s) unrealizable. 1" and red highlighted lines. (Note that there's no pink, that's because of issue #10.) Screenshot: screenshot

My only guess was that there's some leftover file from when this same spec was unrealizable in the past?

cfinucane commented 12 years ago

This surprised me too, at first, but if you scroll up in the "Analysis Output" tab you'll find that it actually says in its entirety:

Specification is realizable. Synthesized automaton is non-trivial. Environment highlighted goal(s) unrealizable. 1 System highlighted goal(s) unrealizable. 1

I asked Vasu about this and she says that this is expected behavior. I'm not entirely clear on why that is, though, so let me forward this on to her.

ConstantineLignos commented 12 years ago

Vasu, can you either change the behavior so we don't see this, or work with Cameron so the UI doesn't show it in the case that the spec is realizable?

vraman commented 12 years ago

Are you using the latest version? Cameron, could you check if this is still happening?

Vasu

On Mon, Mar 19, 2012 at 12:03 PM, Constantine Lignos < reply@reply.github.com

wrote:

Vasu, can you either change the behavior so we don't see this, or work with Cameron so the UI doesn't show it in the case that the spec is realizable?

Reply to this email directly or view it on GitHub: https://github.com/LTLMoP/LTLMoP/issues/11#issuecomment-4576470

ConstantineLignos commented 12 years ago

Vasu, I still see this on the latest version in slurp-dev after building GROne. Is there a change in another branch that needs to be merged into slurp-dev?

vraman commented 12 years ago

Hmm...I just checked out slurp-dev and ran slurptest, and I got the attached aut. Maybe try updating again? Cameron, can you confirm this behavior?

Vasu

On Wed, Mar 28, 2012 at 8:03 AM, Constantine Lignos < reply@reply.github.com

wrote:

Vasu, I still see this on the latest version in slurp-dev after building GROne. Is there a change in another branch that needs to be merged into slurp-dev?

Reply to this email directly or view it on GitHub: https://github.com/LTLMoP/LTLMoP/issues/11#issuecomment-4758087

ConstantineLignos commented 12 years ago

(Attachments don't get sent through github.) There's no problem with the automaton. We always get one and the spec synthesizes successfully. The problem is that when you go to analyze, it says it is realizable and unrealizable. Are you saying that in your analyze window you don't see this? Specification is realizable. Synthesized automaton is non-trivial. Environment highlighted goal(s) unrealizable. 1 System highlighted goal(s) unrealizable. 1

vraman commented 12 years ago

Oh, I see. (Sorry, didn't notice this was through github...blah). Yes, Cameron and I actually talked about this. It's actually an accurate analysis. The spec is realizable because the environment goal is unrealizable, meaning that the system can prevent the environment from fulfilling some goal (the aut we get is a strategy for this purpose). If we used an environment that could not be thwarted in this fashion, the system would be unrealizable and we would not get an automaton.

Does this make sense? I'm happy to write a more detained explanation, but that's the intuition.

Vasu

On Wed, Mar 28, 2012 at 10:02 AM, Constantine Lignos < reply@reply.github.com

wrote:

(Attachments don't get sent through github. There's no problem with the automaton. We always get one and the spec synthesizes successfully. The problem is that when you go to analyze, it says it is realizable and unrealizable. Are you saying that in your analyze window you don't see this? Specification is realizable. Synthesized automaton is non-trivial. Environment highlighted goal(s) unrealizable. 1 System highlighted goal(s) unrealizable. 1

Reply to this email directly or view it on GitHub: https://github.com/LTLMoP/LTLMoP/issues/11#issuecomment-4765388

ConstantineLignos commented 12 years ago

Yes, right, Cameron mentioned that. What I'd like is for us not to show it in the UI when the spec is realizable. (Or choose different colors or something.) Unrealizable and realizable specs look the same in the UI, making demoing bad.

vraman commented 12 years ago

Just being realizable is not enough to ensure that the spec is "good". In this case, the spec may not do what we want it to do because it is actually going after the environment instead of minding its own business. So I think it's appropriate to signal this case as potentially bad. I can see what you mean about it making demoing awkward, but maybe use a spec that is properly realizable (i.e. the system does not have to thwart the environment to win)?

Vasu

On Wed, Mar 28, 2012 at 10:15 AM, Constantine Lignos < reply@reply.github.com

wrote:

Yes, right, Cameron mentioned that. What I'd like is for us not to show it in the UI when the spec is realizable. (Or choose different colors or something.) Unrealizable and realizable specs look the same in the UI, making demoing bad.

Reply to this email directly or view it on GitHub: https://github.com/LTLMoP/LTLMoP/issues/11#issuecomment-4765642

ConstantineLignos commented 12 years ago

I see, what wasn't clear to me is that there's something that could be improved in the spec. What would we need to change in examples/slurptest.spec to make it not be signaled as potentially bad? I'm worried that the answer might have to do with sweep_done, which suggests all our specs will have this problem.

On Wed, Mar 28, 2012 at 10:45 AM, vraman < reply@reply.github.com

wrote:

Just being realizable is not enough to ensure that the spec is "good". In this case, the spec may not do what we want it to do because it is actually going after the environment instead of minding its own business. So I think it's appropriate to signal this case as potentially bad. I can see what you mean about it making demoing awkward, but maybe use a spec that is properly realizable (i.e. the system does not have to thwart the environment to win)?

Vasu

On Wed, Mar 28, 2012 at 10:15 AM, Constantine Lignos < reply@reply.github.com

wrote:

Yes, right, Cameron mentioned that. What I'd like is for us not to show it in the UI when the spec is realizable. (Or choose different colors or something.) Unrealizable and realizable specs look the same in the UI, making demoing bad.

Reply to this email directly or view it on GitHub: https://github.com/LTLMoP/LTLMoP/issues/11#issuecomment-4765642

Reply to this email directly or view it on GitHub: https://github.com/LTLMoP/LTLMoP/issues/11#issuecomment-4766360

ConstantineLignos commented 12 years ago

Fixed by 84abe3e.