CHASE 0.7.2

pip install "chase-cps==0.7.2" (or chase-cps[rtl,z3]).

Long names in the diagrams, and the PDF of a large diagram.

Changed:

• Long names keep the boxes narrow: a title too long keeps the end of its
  path (the part that tells the parts apart: …downstream.baf.bapg_rd)
  and the start of the words after it; a note is broken at its ⊗, · and /
  into three lines at most; a long port name keeps its end. The whole of
  each name is in its tip.
• A check that holds says in its panel what it has shown (for example,
  for M ⊨ C: in an environment that meets the assumptions, every run of
  the model meets the guarantees), not "Holds." alone.
• The wheels are built with less work repeated: the compiled C++ is kept
  between releases, and the tests run in full on Python 3.12 and 3.15 (a
  call of the library on the other versions).

Fixed:

• The PDF of a large diagram had only its top left corner when the page
  was inside a frame, or in a browser that keeps its own paper size: the
  diagram is printed from a page of its own, the size of the diagram, and
  fitted to the page.

CHASE 0.7.1

pip install "chase-cps==0.7.1" (or chase-cps[rtl,z3]).

The diagrams after a review of every demo, and ports of two integer ranges.

Added:

• A variable shared as integers of two ranges (a port of 0..100 feeding one
  of 0..9) is one integer of the union of the ranges. In each contract its
  own range becomes a term: an assumption where it is an input, a guarantee
  where it is an output. The checks then say whether the values fit (a
  counterexample, the term of the range it breaks), and the wire is not
  red. Other types that differ are still an error.

Changed:

• The panel and the waveform float over the diagram, of frosted glass: the
  diagram goes on under them.
• One corner for every box: tags, contracts, the toolbar, the panel, the
  waveform.
• The hole of a quotient is pale yellow, so that it shows when the diagram
  is small.
• A C function with no clause has the contract (⊤, ⊤): its tag is M ⊨ C,
  not safe. The check is the same (no overflow, division by zero, or
  access out of bounds).
• The values of a step are written on the ports over the wires, and the
  same value at the two ends of a short wire once.
• The counterexample table scrolls by whole columns, its end too; long
  lines of code wrap in the panel.
• A quotient by a composition names its parts (Pipeline / (Producer ⊗ Consumer)); a range of one value is written {0}.
• Export: the SVG has the style of each element written on it, so other
  programs (Inkscape, Illustrator, slides) draw it as the page does, with
  its symbols; it has no background. The PNG and the PDF are on white, and
  the PDF is one page the size of the diagram.

Fixed:

• The PDF of a diagram was blank (the rules of the page for printing hid
  it).
• The wires from environments to what they drive could be drawn far above
  the boxes (Deadline): the wires of the top level are placed with their
  row.

CHASE 0.7.0

pip install "chase-cps==0.7.0" (or chase-cps[rtl,z3]).

The waveform of a counterexample, and the panel of a diagram after a try
by three users (a CPS engineer, a hardware verification engineer, a
formal methods researcher).

Added:

• The waveform: the Waveform button of the panel opens the counterexample
  in a drawer under the diagram, as a waveform viewer shows a simulation.
  A row for each variable (those of the requirement first), a column for
  each step; Booleans high and low, numbers as boxes with their values, or
  as a line (Enter). The step that fails is red, the loop is marked ↺ and
  drawn once more, faded. The cursor is the step on the diagram and in the
  table. Zoom (+, −, 0, Ctrl or ⌘ with the wheel), pan (drag, Shift with
  the wheel), the arrows, Alt with an arrow for the next change of a row,
  Home, End, F (the step that fails), L (the loop), Esc; the top edge sets
  its height. In a narrow window it takes the place of the panel.
• A system whose parts do not agree on a signal (driven by two parts, or of
  two types) draws the wires of that signal red, with what is wrong in
  their tip, and warns; its refinement is said not checked, with the
  reason.

Changed:

• Booleans of a counterexample are written ⊤ and ⊥, as in the terms.
• The counterexample is marked at the step where its term is seen to fail:
  G (p -> X X q) at the step of X X q, F[0,6] p at 6, an environment
  at the step where the assumption breaks. A term broken by the whole run
  (F p that never holds) marks no step, and the panel says so.
• A number is never shown rounder than it is (17.996, not 18); the table
  writes short values, with the whole value in its tip.
• The panel: the counterexample at the same place in every problem (titles
  of two lines, headings of one height, the table as wide as the panel, the
  sentences under it); rows of the problems of one height; a check found by
  a core lists its terms (a click shows one on the diagram), with the end
  that sets apart terms that begin alike; "How to fix" names the constants
  that can change, and is worded for each kind of check.
• A problem opened in a large diagram brings its box into view at a size
  that can be read.
• The values of a step stay on the ports inside a box, and read over wires.

Fixed:

• A contract named in Python with a dot or a space (Contract("u_core.alu", ...)) works in the algebra: it is written under a name the language
  takes. A variable with such a name is said before the parser fails.
• A System whose quotient cannot be computed draws the hole with its ports.

CHASE 0.5.0

Added:

• Diagrams (chase_cps.viz, chase-cps view): contracts, components and
  systems drawn as a web page. Refinement is nesting, a quotient is a hole
  with what refines it inside, a component opens on the states of its
  model (RTL through Yosys, JSON, SMV, or a controller), an environment is
  drawn on the left of what it drives, and the results of the checks are
  tags on the boxes, with their cores. Each result of the algebra
  remembers its operands (Contract.origin). Component and System
  bind contracts to implementations; System.check checks each
  implementation and the composition against the contract of the system. The
  page works offline with a local ELK (elk=, --elk); viz.from_spec
  draws a specification file, as chase-cps view does.
• load_dsl(path) reads a problem written in the domain-specific language
  of CHASE (the electric power system patterns of DATE18 and FDL2024) into
  a contract, named after the file (or name=). The graph of the
  architecture is not part of the contract and is skipped.
• to_gr1(c, format="slugs" | "gr1c") writes a GR(1) contract as the input
  of slugs (its structured format) or of gr1c, for users who run a GR(1)
  solver themselves; for gr1c, relations with arithmetic or between
  integers are written as the values that satisfy them.
• chase-cps view reads SystemVerilog Assertions (.sv), writes the data
  of the diagram (--format json), and draws the structure only
  (--no-checks); with --serve, the page takes each new drawing in place
  and keeps its view, and keeps the last diagram when the file cannot be
  drawn. The explanations of the page show in the webview of an editor too.
• chase-cps view --check checks that the assumptions and the guarantees
  of each contract can hold together (A∧G, with the core in red when they
  cannot), and the refinements, implementations, and environments drawn.
  The results are kept next to the file (FILE.results.json, readable
  JSON), found by a hash of what each check reads: a check of contracts that
  have not changed is not run again, and a diagram drawn without checks
  shows the results kept. --budget limits the time of the checks.
• A part not written yet (the contract of a system with some outputs that
  none of its parts drives) is drawn as a hole: the quotient of the
  contract by the parts.
• chase-cps view puts the contracts of a file together by their ports,
  as Lingua Franca does: an output and an input of the same name are wired,
  contracts with the same ports are versions of one part (the first one is
  wired), and a contract whose outputs several parts drive has them drawn
  inside it, its refinement checked with --check (and on save in an
  editor). The MCP tool visualize checks these refinements by default.
• chase-cps view --implementation MODEL C draws C as a component with
  its model (SMV, JSON, or RTL read with Yosys), checked with --check; a
  Verilog or SystemVerilog file with no assertions is drawn as its module.
  The options of view can be written at the top of the file
  (# view: ..., // view: ... in Verilog). The page saves the diagram as
  SVG, PNG, or PDF, and in an editor a double click on a box, or on a term
  (of a core, for instance), goes to its line in the file.
• RTL read with Yosys finds the files named by `include next to the
  sources, not only .svh and .vh headers.
• chase-cps view of a Verilog module that uses modules of other files
  takes the files next to it that have them.
• The checks keep their results on the contracts they check, with what the
  contract said then (Contract.checked()): a diagram draws them with no
  checks=, and drops them when the contract changes.
• A name that is not declared in a specification file is reported with
  its contract and its line.
• viz.diagram(..., open=[...]) and chase-cps view --open draw boxes open
  when the page loads: the terms of a contract, the states of a small
  model, and the core of a check that fails.

Changed:

• Demos: AIAgents is now PaymentAssistant; DATE18 and DATE21 use slugs
  instead of gr1c; DATE18/eps.py checks the power system in Python; the
  READMEs show each step with its diagram, as the website does.
• ensure of a contract without assumptions keeps its terms: (true, G and
  the new guarantee), the same contract as before, instead of the saturated
  formulas of the composition.

Fixed:

• A copy of a temporal formula lost its interval, so an operation of the
  console (compose, for instance) turned G[0,2] p into G p.
• The console commands stl and synthesize crashed without a contract,
  or with the name of no contract.
• synthesize C file gr1c wrote a broken file when a relation compares
  two variables or has arithmetic, which gr1c cannot read; it now writes
  nothing and says to use to_gr1(c, format="gr1c").
• R (release) in a specification file crashed the parser of logics_tool
  (exit code 134 or 138): it built only U.
• The interval of a temporal operator in a specification file
  (G[0,3] p, x U[1,2] y) was dropped, so G[0,3] p was read as
  G p. The Python package now unfolds it into X, and refuses an
  interval that is not a range of whole steps, and X[a,b].
• A probability, P(...), now gives the name of the contract and says
  that probabilities are not checked, instead of a traceback.
• A negative constant (w >= -0.8, n > -3) made the operations computed
  by the C++ library (composition without discharge, for instance) fail
  with "Invalid number format": the logics language reads -0.8 as one
  token and rejects it. The formulas are now written with (0 - 0.8).

CHASE 0.4.2

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.

CHASE 0.4.1

New:

• RTL (chase_cps.rtl): Model.from_rtl(files, top) reads a Verilog or
  SystemVerilog module with Yosys as a state machine, for implements,
  accepts, and is_receptive. The ports are the variables of the
  contracts (1 bit: Boolean, more: words); reset holds the reset in the
  first step; names renames ports. pip install chase-cps[rtl] installs
  Yosys (yowasp-yosys, ISC license).
• merge(..., discharge=True) and divide(..., discharge=True): the result
  keeps the terms of the contracts and is the same contract as the closed
  form, then the redundant terms are dropped. The merge is (A1 & A2,
  G1 & G2); the quotient assumes A1 and the guarantees of the part (under
  the assumptions of the part that A1 does not imply), and guarantees G1
  and the assumptions of the part. The results can go to is_realizable
  and synthesize, which do not take the closed forms.
• Demos: BufferSwap (a buffer of a circuit replaced, with the contracts in
  SVA and the RTL of BaseJump STL), LMFSM (the state machine of the Ten
  Lockheed Martin Cyber-Physical Challenges), and AHB (the arbiter of the
  AMBA AHB bus as two viewpoints in SVA).

Fix:

• parse_sva read the assertions inside generate blocks, those of both
  branches of a generate if; they are skipped, with the reason.

CHASE 0.4.0

New:

• Words (chase_cps.words): unsigned and signed bit vectors of a fixed
  width, "word[8]" and "signed word[8]", as in nuXmv and SystemVerilog,
  with the arithmetic modulo 2^n. Operators: + - * / mod, the bitwise
  & | xor !, the shifts << >>, the concatenation ::, and the bits
  x[7:0], x[3] (a single bit is a Boolean). A formula whose operands do
  not have the same width and signedness, or a constant that does not fit,
  is refused when the contract is built. The checks give the words to nuXmv;
  the values of the traces are integers. extend(x, n), signed(x), and
  unsigned(x) change the width and the signedness, as in nuXmv. The
  contract algebra works on
  contracts with words: each comparison over words goes to the core library
  as a Boolean variable and comes back after the operation (the results are
  the same as on integers). State machines may declare words. Not in the
  logics language (to_spec) and not for slugs. MCP server: the types
  "word[n]" and "signed word[n]".
• SystemVerilog Assertions (chase_cps.sva): parse_sva reads the
  assume property and assert property statements of a text as a
  contract, with the widths of Verilog, $past and the functions on it,
  sequences of bounded length, disable iff, named properties and
  sequences, and definitions; the statements not read are listed with the
  reason. to_sva writes a contract as a checker module (and a bind
  statement). Packed arrays of several dimensions are words; hierarchical
  names (u1.state) are read as one name (u1__state, mapped back in
  names). The meaning is that of the standard (IEEE 1800-2017, Annex F
  for disable iff), not that of a tool. Tested against a reference
  interpreter of the standard, against Verilator, and against Jasper.
• past(x, n): the value of x n steps before (any value in the first n
  steps), for variables of any type. nuXmv gets it as history variables;
  the contract algebra treats a formula with it as one proposition; slugs
  and the logics language do not take it. parse_sva writes with it the
  comparisons of values two cycles apart or more (y == $past(x, 2)).
• The engine of nuXmv can be chosen: engine="portfolio" (the default),
  "ic3", "bdd", or "bmc", or in the back end, "nuxmv/bdd", as the
  results name it. Command line: --engine. engine="ic3" with NuSMV and
  an unknown engine are refused (before, they ran BDDs).

Changes:

• nuXmv runs IC3 and BDDs at the same time by default (portfolio; before,
  IC3 alone): the first verdict wins. BDDs are much faster than IC3 when a
  counterexample needs a long loop. The verdicts are the same; a
  counterexample may differ from one run to the next, and the one of BDDs
  can be a loop without a prefix.
• MCP server: the tools have the names of the Python functions:
  parse_spec and to_spec replace read_spec and write_spec, and
  parse_sva, to_sva are new.
• mod and xor are keywords of the formulas: they cannot be names.

Fixes:

• Variables named as keywords or functions of nuXmv (count, abs,
  next, init, E, ...) made nuXmv fail with a syntax error; they are
  renamed in the models given to it.
• IC3 of nuXmv 2.2.0 gives wrong answers on formulas with signed() and
  unsigned() (it finds G X (s < signed(x)) -> X G (s < signed(x))
  false); these formulas are checked with BDDs.

CHASE 0.3.2

Changes of behavior:

• verify checks that the assumptions and the guarantees can hold together
  (A & G satisfiable). This implies compatibility and consistency, which it
  still reports; before, a contract whose guarantees cannot hold when its
  assumptions do passed verify (A -> G holds when A fails). With
  core=True an unsat result carries the terms that conflict. On the 513
  contracts of the ContrAgent libraries, the results are the same. The
  console verify command writes a third LTLSPEC, the negation of A & G.
  chase-cps check without options prints one verify line per contract.
• is_well_separated keeps the initial and safety guarantees of the
  component by default (with_guarantees=True, Maoz and Ringert, Def. 4):
  a violation of the assumptions that the component can force only by
  breaking its own guarantees is not a defect of the assumptions.
  with_guarantees=False gives the check of before.
• remove_vacuous is removed: it is a removal of redundant terms, and is
  now remove_redundant(c, synth=True), which keeps realizability and the
  controllers (remove_redundant(c) keeps A -> G, as before). The result
  is a Redundancy, with the removed terms (RedundantTerm: part, and
  kind with synth). Vacuity and VacuousTerm are removed. "Vacuity" is
  now only is_vacuous.

New:

• is_vacuous: vacuity in synthesis (Bloem, Chockler, Ebrahimi, and
  Strichman, FMSD 2021). Can the component win without an output that a
  liveness guarantee asks for, never or from some step on? With the
  strategy, and with core=True the assumptions that allow it. The queries
  are those of the exact vacuity checks of ACIES.
• remove_redundant(c, core=True): each removed term comes with a minimal
  set of the terms that imply it.
• State machines (chase_cps.models): a Model from SMV text or a file,
  from a controller of synthesize, or from a state machine in JSON.
  implements and accepts take them, and is_receptive checks that a
  model does not refuse the inputs that the assumptions allow (the state
  and the input when it does). synthesize keeps the initial terms of the
  contract with the controller, since slugs does not mark the initial nodes.
• chase-cps check: --implements MODEL C, --receptive MODEL C
  (an SMV or a JSON file), and --vacuous C.
• MCP server: the tools is_vacuous and is_receptive; implements and
  accepts take a state machine (smv, machine, controller);
  remove_redundant takes synth and core, and the tool remove_vacuous
  is removed. The skill says when to use each operation and check.

Faster:

• An implication check of one term against other terms uses only the terms
  that share variables with it, directly or through other terms, when all
  of them are satisfiable (checked once): the answer is the same.
  Composition with discharge and remove_redundant give the same results.
  RoboticJoints, composition with discharge of 8 joints: 140 s in 0.3.1,
  21 s (demos/RoboticJoints/results/discharge_speedup.csv).

CHASE 0.3.1

• The Python package, its documentation, the command line, and the tools of
  the MCP server are organized in three layers:

  1. contracts and their algebra (chase_cps.contract), which hold for any
     assume-guarantee contracts;
  2. checks: on contracts (chase_cps.checks: refines, verify,
     is_compatible, is_consistent, implements, accepts, remove_redundant),
     and the queries on formulas they reduce to (chase_cps.logic:
     implies, is_satisfiable, unsat_core);
  3. GR(1) synthesis with slugs (chase_cps.gr1: is_realizable,
     synthesize, unrealizable_core, is_well_separated, remove_vacuous).

  All the names are still in chase_cps, and the modules of 0.3.0
  (chase_cps.checks, chase_cps.cores) still give them: no code has to
  change. docs/usage.md has a section and a table for each layer.

• The documentation says what each query checks: implies the validity of
  an implication, is_satisfiable the satisfiability of a formula, which is
  not the satisfaction of a contract by a component (implements).

• chase-cps check --help groups the options: checks on contracts (nuXmv),
  GR(1) synthesis (slugs).

• Release: ccache keeps the C++ objects between the builds of the Python
  versions, and a tag builds the wheels once and uploads them to TestPyPI;
  once they are checked, a manual run publishes the same files to PyPI.

CHASE 0.3.0

• context=: formulas that every behavior satisfies (the axiom of an
  encoding of finite traces, a physical law), for the checks built on
  implication and satisfiability: implies, is_satisfiable,
  is_compatible, is_consistent, verify, refines,
  remove_redundant, accepts, implements, and unsat_core, also in
  the MCP server. The behaviors that violate the context are left out; as
  an assumption, the context would not help, since a behavior that
  violates an assumption satisfies the contract. See "Context" in
  docs/usage.md.
• load_spec and parse_spec warn when an integer is compared with a
  constant outside its range (e.g. credits >= 90 with credits declared
  without a range, so 0 to 16): the comparison has the same value at every
  step.
• The operations no longer leak memory. Before, every operation in Python
  (and every contract read from a file) kept the objects of the core
  library for good, 2 to 16 KB per operation. Now a contract owns its
  declarations and formulas, and a formula its operands, and chase_cps
  frees the objects of the core library once it has read the result
  (pychase.utilities.destroy). logics_tool: a proposition defined by a
  relation (proposition p is x > 3;) gets its own copy of the relation
  at each use, and a contract its own copy of the declarations of the
  system it uses.
• Core library: refinement put the formulas of the two contracts in the
  result instead of copies of them; saturating a contract with assumptions
  and no guarantees crashed (logics_tool saturate); the simplification
  turned a LargeOr of two formulas into an and.
• DSL_tool: computing the precision of the timings read one value past the
  end of an array (found by AddressSanitizer); the result was not used, and
  the specifications it writes are the same.
• CI: a job builds CHASE with AddressSanitizer and runs the Python tests
  and the console scripts of the demos.