search

SNSystems / dexter

DExTer - Debug Experience Tester
MIT License
33 stars 6 forks source link

Implement DexVerify and LTD #30

Closed OCHyams closed 5 years ago

OCHyams commented 5 years ago

IMPORTANT:

  1. I don't intend to get this work merged as is. This is a review/RFC PR.
  2. Please read the LTL_work.md document for more details.
  3. This commit implements Expect(var, value) -- this will be replaced with a full program state command.
  4. The --verbose option doesn't output very useful info for DexVerify. The Heuristic class needs a lot of work before I can do anything here (I have some stashed work on this).

  5. The result is only pass or fail -- the model either holds or it does not.

    DexVerify is a dexter command which can be used to verify a proposition about the program trace.

A proposition can be made up of atomic propositions (assertions about what the program state) and propositions (recursive!), connected by operators. The operators can be boolean or temporal. The terminology and theory behind this is explained in the document LTL_word.md included with this commit.

The term LTD is used to describe the DexVerify subcommands which are based on Linear Temporal Logic (LTL).

OCHyams commented 5 years ago

I intend for the dexter/examples/ directory to contain examples but for this work I've been using it as a sort of regression test set.

OCHyams commented 5 years ago

The proposition (p After q) literally means "p holds after q holds". Because of the prefix notation, After(p, q) reads as "after p holds, q holds" - to me at least - which is of course incorrect (it is actually "after q, p holds").

I've kept the operands in this order to match the other temporal binary operators.

I think there's a serious case for swapping all the binary operator operands to make parsing the prefix notation easier (for humans). The downside is that this could really confuse people who regularly see prefix notation and those who know LTL well already.

OCHyams commented 5 years ago

I'll avoid updating this with my up to date changes until #31 is accepted.

OCHyams commented 5 years ago

I'm closing this because it's now quite out of date. I'll put up another PR soon.