Skip to content

CHASE 0.4.2

Choose a tag to compare

@yfxiao16 yfxiao16 released this 29 Oct 03:07
· 187 commits to master since this release

Changed:

  • is_implementation(m, c) and is_environment(e, c) are the new names of
    implements(m, c) and accepts(c, e), after the terms of the theory
    (M is an implementation of C, E is an environment of C); the environment
    now comes first, as the implementation. The old names still work, with a
    DeprecationWarning. Command line: --implementation MODEL C (was
    --implements, still read) and the new --environment MODEL C. MCP
    server: the tools are named is_implementation and is_environment.

New:

  • conjoin(..., discharge=True): the result keeps the terms and is the
    same contract as the conjunction. Each guarantee is guaranteed under the
    assumptions of its contract that the other's do not imply; when the
    assumptions of one contract imply those of the other, the assumption is
    theirs and has no disjunction (with the same assumptions, (A, G1 & G2)).
  • Docker image published on ghcr.io/chase-cps/chase at each release
    (docker pull ghcr.io/chase-cps/chase), without nuXmv, whose license does
    not allow redistribution: the checks use NuSMV, built from its sources
    without zChaff (LGPL), and chase-cps install nuxmv --accept-license adds
    nuXmv in a container. The image also has Yosys (yowasp-yosys) and the
    chase-cps command; the demo suite runs Charger, LMFSM, and AHB with
    NuSMV, and BufferSwap.
  • chase-cps install nusmv says that the build of FBK is linked with
    zChaff, for non-commercial use only.
  • CONTRIBUTING.md: reporting bugs, building and testing, and proposing
    changes.