Closed jrbeaumont closed 7 years ago
I didn't have a chance to have a look at this PR as I was very busy this week.
After a brief look: that's way too much code duplication. There appear to be completely identical files, like FSM.Abstract
and STG.Abstract
. Why not have a single file instead?
I agree with this, I was working on it and found the latest error and fixed it.
I accidentally completed and closed the pull request which I've only just realised.
It does work at least. But yes, I think a Concepts.Abstract
would be a better idea, something that both STG and FSM translation can use, and then when they do diverge, this Concepts.Abstract
can be built upon in STG.Abstract
etc.
My major idea at the moment is to build upon Concepts.Abstract
with FSM.Abstract
to include invariants.
My major idea at the moment is to build upon
Concepts.Abstract
withFSM.Abstract
to include invariants.
I think invariants should eventually be supported by both FSM and STG concepts. The latter will generate properties from invariants (to be checked by Workcraft), so I'd propose to add them in a unified manner to both, perhaps with a warning that they are not yet supported by the STG translation.
I accidentally completed and closed the pull request which I've only just realised.
I think you could try reverting the merge commit and see what happens :-)
I think you could try reverting the merge commit and see what happens :-)
I cannot see the revert button, maybe you can? My repo seems to not be up to date, i'm worried I pushed to the wrong repo by accident :S Maybe giving me higher permissions was a mistake haha
so I'd propose to add them in a unified manner to both
I assume you mean within their separate files, i.e. FSM.Abstract
or STG.Abstract
. This can be arranged, and I will get on with it :)
Yep, looks like you've been pushing to master directly :)
I assume you mean within their separate files, i.e. FSM.Abstract or STG.Abstract.
No, I meant a single file, shared by both FSM and STG concepts. I don't see any reason to keep them separate, as identical files in the repo.
Yep, looks like you've been pushing to master directly :)
A silly mistake :S Sorry!
No, I meant a single file, shared by both FSM and STG concepts. I don't see any reason to keep them separate, as identical files in the repo.
What I mean is have a single set of files: Concepts.Abstract
and Concepts.Circuit
. When adding an implementation of invariants, have a STG.Circuit
just for the implementation of invariant for STG, and FSM.Circuit
for invariant of FSM. They will have differing implementations so they will need separate files.
I intend on setting up the single files and sending a PR for that, for review, and then adding invariant so you can review that separately.
@jrbeaumont Sounds good, go ahead!
ARandomOWL implemented the FSM translation.
I integrated it, added an option for this and tested.
I also did some refactoring to allow uniformity between STG and FSM translation, and so automated testing of STG translation would work correctly.