Skip to content

Imperative NondetStmt should be merged into Stmt #383

@MikaelMayer

Description

@MikaelMayer

Instead of having two ASTs, one for nondeterministic statements and one for deterministic statements, we should have only one AST.
There are several reasons for that

  • We would be able to selectively convert deterministic statements to non-deterministic ones.
  • The "deterministic statement" can already reference non-deterministic commands such as havoc, which make it possible to already emulate the nondet choice. Same for the loop which can be emulated via a regular loop and a havoc command.
  • If at any point we prefer to have only recursively nondeterministic statements, we could merge the ASTs and have a predicate instead of a type.
  • Any change in statements does not need to be reflected in the nondeterministic statements, such as addition of new AST nodes or changes of semantics. Less maintenance and possible duplication. We have a few upcoming changes to statements: function declarations, procedure declarations, type declarations

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions