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

The output format of fsa.stateToLTL is wrong #53

Closed wongkaiweng closed 10 years ago

wongkaiweng commented 10 years ago

CURRENTLY: def stateToLTL(state, use_next=False, include_env=True, swap_io=False): """ swap_io is for the counterstrategy aut in mopsy """

def decorate_prop(prop, polarity):
    if int(polarity) == 0:
        prop = "!"+prop
    if use_next:
        prop = "next({})".format(prop)
    return prop

OUTPUT WILL BE : next(!prop) --> different from current .ltl output

SHOULD BE CORRECTED TO def stateToLTL(state, use_next=False, include_env=True, swap_io=False): """ swap_io is for the counterstrategy aut in mopsy """

def decorate_prop(prop, polarity):
    if use_next:
        prop = "next({})".format(prop)
    if int(polarity) == 0:
        prop = "!"+prop
    return prop

OUTPUT WILL BE: !next(prop)

cfinucane commented 10 years ago

You are correct, a lot of things (particularly the code dealing with converting from LTL to SAT) assume that next() only operates on bare propositions. Ideally we should not care about specific representations of equivalent LTL formulas, and this can be fixed programmatically by normalization (e.g. see 6b24c87c1a230ab44778dd43ee83f1cfd088f95e, which is not yet merged to dev), but for now your fix is absolutely appropriate. Would you mind submitting this patch as a pull request?

wongkaiweng commented 10 years ago

Ok. I created a pull request~

2014/1/20 Cameron Finucane notifications@github.com

You are correct, a lot of things (particularly the code dealing with converting from LTL to SAT) assumes that next() only operates on bare propositions. Ideally we should not care about specific representations of equivalent LTL formulas, and this can be fixed programmatically by normalization (e.g. see 6b24c87https://github.com/LTLMoP/LTLMoP/commit/6b24c87c1a230ab44778dd43ee83f1cfd088f95e, which is not yet merged to dev), but for now your fix is absolutely appropriate. Would you mind submitting this patch as a pull request?

— Reply to this email directly or view it on GitHubhttps://github.com/LTLMoP/LTLMoP/issues/53#issuecomment-32818208 .

Catherine (Kai Weng) Wong Cornell University | Mechanical Engineering Class of 2013