Skip to content

CHASE 0.1.2

Choose a tag to compare

@yfxiao16 yfxiao16 released this 26 Oct 03:22
· 231 commits to master since this release
  • The slugs back end wrote the constants true and false as nothing, so
    G F false became an empty liveness condition and any term with a
    constant was written wrongly. It now writes them, and a formula node it
    cannot write is reported instead of skipped.
    The gr1c back end of logics_tool had the same problem with the constants.
  • A new test writes contracts for slugs, compiles them with the slugs
    compiler, reads them back, and checks with nuXmv that the assumptions and
    guarantees read back are equivalent to those of the contract, for fixed
    cases and for random contracts (CHASE_SLUGS_FUZZ).
  • The comparison with Pacti is no longer in the documentation.