search

equivio / silent-step-spectroscopy

Isabelle formalization of linear-time–branching-time spectroscopy accounting for silent steps
https://equivio.github.io/silent-step-spectroscopy/AFP/LinearTimeBranchingTimeSpectroscopyAccountingForSilentSteps/index.html
Other
0 stars 0 forks source link

Change HML_SRBB Definition to exclude tau from Obs steps #49

Closed ekeln closed 11 months ago

ekeln commented 11 months ago

Currently, the definition allows for formulas to check for visible tau steps, this is wrong.

The approach is to change the definition to "soft_pos", but we have to check if this is correct.

benkeks commented 11 months ago

@ekeln @betawave Is this a separate issue or will you combine it's treatment this with #28 ? (If the first, then you should create a PR for your branch here.)

betawave commented 11 months ago

This will be close by https://github.com/equivio/silent-step-spectroscopy/pull/41