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).