CHASE 0.2.0

• Implication and coimplication of contracts (the adjoints of conjunction
  and disjunction), the reciprocal, and the two Boolean actions that add an
  assumption or a guarantee (Incer, Benveniste, Sangiovanni-Vincentelli,
  arXiv 2309.08875). In the core library and the console of logics_tool
  (imply, coimply, invert), and in Python and the MCP server (imply,
  coimply, invert, assume, ensure).
• compose(..., discharge=True): composition that keeps the terms of the
  contracts and drops the assumptions discharged by the other contract and
  the redundant terms (Incer, PhD thesis 2022, Algorithm 2). When the
  contracts feed each other, the assumptions are discharged in one
  direction only, the one that drops more of them.
• Cores: unrealizable_core (with slugs, QuickCore order) and unsat_core
  (of A & G, with nuXmv), from a contract or from formulas, and core=True
  on is_realizable, is_compatible, is_consistent, and is_satisfiable;
  chase-cps check --core.
• is_well_separated: whether the component can win by forcing the
  environment to violate its assumptions, with the strategy and a minimal
  set of assumptions; chase-cps check --well-separated.
• remove_vacuous: removes the terms whose removal keeps the GR(1)
  specification (inherent vacuity, Maoz and Shalom 2020), with the kind of
  each term and the terms that make it vacuous.
• The GR(1) back end reports a contract whose variables do not have the
  roles of slugs (an initial assumption that reads an output, a safety
  assumption that reads the next value of an output) before calling slugs,
  with the term.
• load_spec and parse_spec: the variables declared outside the contracts
  are given to the contracts that use them. Before, they were left out of
  the inputs and outputs of the contracts.
• A temporal operator applied to an operand of a relation or of arithmetic
  (X x = 3) is rejected with a message (write x' = 3).
• Real variables ("real", real variable x; in the CHASE language) and
  numbers with a fraction (20.5), read exactly. Before, a real variable
  was read as a Boolean one and 20.5 as 20; a real constant was read as
  an integer (real constant K 2.5; gave 2). The checks handle real
  variables in this order, and say which way answered (reals):
  regions, exact, when the real variables are compared with constants or
  with each other, without arithmetic (also for realizability and
  synthesis, with the controller written with the conditions on the real
  variables); the SMT engine of nuXmv; predicate abstraction, which
  returns only the answers that hold for the real variables, refined with
  z3 when it is installed (pip install chase-cps[reals]). See "Real
  variables" in docs/usage.md. Without real variables the checks are
  unchanged.
• The NuSMV printer of chase-backends writes real variables (with their
  range as INVAR) and real constants for nuXmv; the slugs and gr1c printers
  report real variables instead of writing them as Boolean ones.
• logics_tool: refinement (and the other operations) crashed when a
  contract used a variable declared outside the contracts. A contract now
  declares the declarations of the system it uses, and the NuSMV printer
  writes the constants (DEFINE), which it skipped.
• nuXmv no longer waits at its prompt after an error until the timeout: the
  error is reported at once.
• logics_tool: verify and refinement say when the file they write has
  real variables or real numbers, which only nuXmv reads (go_msat, then
  check_ltlspec_ic3); the file starts with a comment that says the same.
• The example of the README and of the page of the package on PyPI used
  refinement, which is refines since 0.1.0. A new test runs the Python
  examples of the README files and of docs/usage.md, and checks that the
  names in the table of the operations exist (Python, chase-cps check, and
  the console of logics_tool).
• A syntax error in a specification (load_spec, parse_spec, chase-cps check, the MCP tool read_spec) gives the line, the column, and the
  token in the message; before, the parser wrote them on the standard error
  only, and parse_spec named a temporary file.
• A variable type that is not bool, real, or (low, high) with integer
  bounds is reported with the type ('integer' was shown letter by letter,
  and [1.5, 3] was read as (1, 3)).
• New demos: Charger (unrealizable core, synthesis, well-separation,
  vacuity, and composition with discharge of an arbiter and two robots)
  and LiftPlusCruise (requirements of the FRET case study with real
  variables: consistency, a behavior, and the requirements in conflict).
  The demo suite runs both.

Known issue: the operations of the core library (composition, conjunction,
quotient, ...) do not free the memory they use, about 10 to 15 KB per
operation (about 9 KB in 0.1.2). A later version will.