Open spmaniato opened 9 years ago
Similar idea: synthesize SM that only has failed
outcome. If all goes well, it cycles through goals infinitely often. If something fails, it returns the outcome. It mixes infinite with finite execution.
Edit: This seems to work as expected with a manually created SM. I now have to add support for LTL generation with a single failed
outcome.
I like the idea of solely having a failed outcome, just to cover the case when the robot would not be able to recover.
You are right, it is not possible to have no outcomes. However, you don't need to connect your single dummy outcome.
"execute an infinite run and show a simulation of that" Good luck, may take a while... :P
By the way: What is the reason you use GR(1)? Are there any relevant disadvantages of co-safe LTL?
What is the reason you use GR(1)? Are there any relevant disadvantages of co-safe LTL?
Yeah, co-safe LTL would be a very logical choice as well. I actually have a note that says I should address this point in the Introduction of the paper. Because the reviewers will question this choice too.
In brief, we don't want to lose the expressivity of GR(1) just because the DRC tasks happened to be finite. Also, co-safe LTL doesn't give you reactive mission plans (in the adversarial environment sense). So far we've only been reacting to failures and in a trivial manner. But GR(1) can handle reaction to sensors and external events in a provably-correct manner.
Super-failed attempt at "infinite execution if all goes well", "fail otherwise" ... :disappointed:
The LTL synthesis part works as expected. However, the semantics of the synthesized automaton are so different from FlexBE's that the SM Generation step "freaks out". I'll spend some more time on this but I will abort if I haven't made significant progress by next Wednesday (09/09).
Is this on FlexBE's side / do I have to fix something? What does the StateInstantiation message say?
I don't see a particular difference from other statemachines. FlexBE does not interpret any outcomes. So from this point of view, it also could be a statemachine which cannot fail (only outcome: finished) because any internal failure is handled properly or simply ignored and I already defined such statemachines multiple times.
No, don't worry. The problem is with going from the (quite different than before) synthesized automaton to the state machine (i.e., the StateInstantiations). I'll have to revise the SM Generation step quite a lot.
Jon pointed out that a reviewer of the ICRA 2016 paper might argue that something like co-safe LTL would make more sense for the finite tasks we had ATLAS perform (as opposed to me adding more GR(1) formulas to make the synthesized automaton behave like a finite run)
The first step is to manually create a state machine with no outcomes in FlexBE to see whether it complains. Edit: It does complain. See #3174