release v2026.08.30

CHANGELOG.rst

@@ -1,6 +1,90 @@
 Change log
 ==========
 
+v2026.08.30
+-----------
+
+User-facing changes
+~~~~~~~~~~~~~~~~~~~
+* Bug fix: passing a ``--value-type`` containing spaces to ``murphi2c`` no
+  longer results in malformed code (commits
+  7feb6e0aa0b2b079c2e4f00cc5ceb519d9dac6e6,
+  e38ce1b5f02beb7f996fac5ff5e64673ca323f20,
+  a1d416ec999af9c24de218942b35fa3cb7f6fbbb).
+* Bug fix: ``murphi-format`` more correctly handles ``==>`` followed by
+  ``begin`` with multiple newlines in-between (commit
+  70173dbe7adb55faa6de5e3fba24522fa3beb4e6).
+* Bug fix: monitoring of subprocesses (SMT solvers) was corrected, avoiding a
+  previous possible deadlock (commit 67c545f43eb8a71fc59465d8f2d9227a9dd7d631).
+* Bug fix: ``murphi-format`` recognises the command line option ``-h`` (commit
+  dc03b1031931030fd0cb9b7074a4ad345dee5bb5).
+* Bug fix: ``murphi-format`` recognises the command line option ``-t`` (commit
+  9e47b916f8f208a4bfe36ffdafc094caa37745d9).
+* Bug fix: when passing a very small number to ``--set-capacity``, malformed
+  code is no longer generated (commit 80f9ac2acbe3db43bb09fd8fba4e87b4f85fd57b).
+* Bug fix: ``murphi-format`` recognises and responds to failures to rewind file
+  pointers (commits 52eed93e005726fd39b7ad7327c35acba1afc386,
+  79be8baacb001a3180c77f5ef89ffccb309a5641).
+* The ``undefined`` keyword is now supported (commits
+  1c419e523f625b8ff4d31cd33f9a9fb021f6ed42,
+  dd3bc59f781c8ae587f3a5753b80ed06ac033c8b).
+* The ``union`` type is now supported during parsing and type checking. It is
+  still not possible to generate a checker from a model containing unions but
+  some auxiliary tools like ``murphi2xml`` fully support unions. The main
+  purpose of this addition is to support third-party code using librumur to
+  parse union-containing models (commits
+  7ecea100928755fb5f5cb37b638799177b3114c1,
+  3b58aa9dbfae7082c01b36368785fea530717e31,
+  d6b7949fea8c9da3bdbd08d0311b60fca04683cc,
+  62a8c4931edc787401726f2e17d40d4832836d0d,
+  c8720b77e298e51350be5486829f16f2c2bf15e8,
+  c89bd8afdaa1aad2089cecfb7a77d2e28fab68a4,
+  5a2545ee489faf4b730e00797b97979e53b3fab2).
+* The ``multiset`` type is now supported during parsing and type checking. It is
+  still not possible to generate a checker from a model containing multisets but
+  some auxiliary tools like ``murphi2xml`` fully support multisets. The main
+  purpose of this addition is to support third-party code using librumur to
+  parse multiset-containing models (commits
+  9f55ca0ed6fbf0b841130f2c71e5bbf69d4957d0,
+  0b3e81a6b425d10f5847e8907cf36487944cc017,
+  0639e869deb55f9930e485a5029c82316eafc950,
+  1942fbaab08493e2a02a02cb1ef3af40b1901cd9,
+  b9d77afccfc01ce9be1287580714c8dd3934493c,
+  dbd173eefe7ab88b329330d58c214169133aca46,
+  df05e0f8df35146f535cc42cc134cd2efbb47735,
+  c12c449c53600e8de09fb40459f67590d8399990,
+  ba7239c495f448f60977c6059af2f14d16fb509a,
+  8eb2b08949f5c2c97ee3dc5f22594c5ffbd1fc39,
+  1076e5f55a0e164824a4e1c23f0ad0fd33528dd1,
+  d1cfbdd8a8b1cf96e9f265bcc4061b2ecb26205f,
+  d70d11730bd472b36f96fc6539a4a05b2c881fd4,
+  67127631f48b6f495d858bae6a52de4b0dcaf0ae,
+  e534adfddbfa43ee0d572a96a3aa718d8a7bfec2,
+  745ce5eec26b43a123ba27e9f7403fd511022307,
+  666b89cdfb62af4d39fb292ebe74625715c7a69b,
+  2a686b72ac14948168f58957bff44a7898891cec,
+  f6617bef7bab564139822149caafd67b0c722614).
+* ``--help`` ignores ``$TMPDIR`` when it points to an unusable directory (commit
+  b873e30df7b7f14af3529dd0a2355f8b91d6956e).
+* A false positive ``-Wshift-count-overflow`` compiler warning when building the
+  generated checker with GCC ≥ 15 has been suppressed (commit
+  11347fc61465d5aa7c46fb21721a8cf579739e38).
+
+Internal changes
+~~~~~~~~~~~~~~~~
+* Bug fix: array indexing (``Element``) is considered impure (``is_pure()``
+  returns ``false``) if its indexing expression is impure (commit
+  2eb8c356927601e6ac4ef0120746da9ebb702ea8).
+* Bug fix: array indexing (``Element``) is considered impure (``is_pure()``
+  returns ``false``) if its array expression is impure (commit
+  b0aa51f9631457fb9992d0ef19229197678a9c2f).
+* Bug fix: record field selection (``Field``) is considered impure
+  (``is_pure()`` returns ``false``) if its left-hand side is impure (commit
+  d6c04d2a15021338e29e5c80bb940e0993c87a1c).
+* The ``lower_bound`` and ``upper_bound`` member functions on AST nodes now
+  return ``mpz_class`` values instead of ``std::string`` values (commit
+  fd2a59a25af8c4a45f6ec85303c6bad9260a069e).
+
 v2026.03.11
 -----------
 

share/CMakeLists.txt

@@ -20,3 +20,6 @@ install(DIRECTORY v2025.08.31
 install(DIRECTORY v2026.03.11
   DESTINATION ${CMAKE_INSTALL_DATAROOTDIR}/rumur/lib
 )
+install(DIRECTORY v2026.08.30
+  DESTINATION ${CMAKE_INSTALL_DATAROOTDIR}/rumur/lib
+)

share/v2026.08.30/_list

@@ -0,0 +1,232 @@
+dnl template for a statically sized list/queue/stack
+dnl
+dnl This file defines, as an M4¹ template, a type-generic Murphi list data
+dnl structure. To use this, include the template and then call the macro "_list"
+dnl with 4 parameters:
+dnl   • "name" – a prefix for the generated list data structure and its
+dnl     supporting functions
+dnl   • "index_t" – a Murphi type for indexing the list
+dnl   • "elem_t" – a Murphi type for the elements of the list
+dnl   • "size" – one more than the number of elements in type "index_t",
+dnl     defaulting to 2³¹-1 (see discussion of this below)
+dnl E.g.:
+dnl
+dnl   include(`_list')dnl
+dnl
+dnl   type
+dnl     int: 0..32;
+dnl
+dnl   _list(`ints', `0..10', `int')dnl
+dnl
+dnl Pre-process your model with M4:
+dnl
+dnl   $ m4 --include=/path/to/rumur/install/share/rumur/lib model.m >out.m
+dnl
+dnl This generates a type and some supporting functions:
+dnl
+dnl   type
+dnl     ints_t: …
+dnl
+dnl   function ints_is_empty(list_: ints_t): boolean;
+dnl   function ints_is_full(list_: ints_t): boolean;
+dnl   function ints_size(list_: ints_t): 0..2147483647;
+dnl   procedure ints_push_back(var list_: ints_t; elem_: int);
+dnl   function ints_try_push_back(var list_: ints_t; elem_: int): boolean;
+dnl   function ints_pop_front(var list_: ints_t): int;
+dnl   function ints_pop_back(var list_: ints_t): int;
+dnl
+dnl You can then go on to use the "ints_t" type in your handwritten model code.
+dnl
+dnl "index_t" can be an arbitrary type; the only requirement is that it is
+dnl iterable. It can be a previously defined type or a type literal. The
+dnl underlying type could be boolean, a range, a scalarset, or an enum. Though
+dnl it is unlikely anything except a range makes sense.
+dnl
+dnl "elem_t" can be an arbitrary type. It can be a previously defined type or a
+dnl type literal, though you probably want to name it in order to more easily
+dnl use the push and pop functions.
+dnl
+dnl "size" does not need to be supplied unless (a) your indexing type "index_t"
+dnl has more than 2³¹-2 elements or (b) you are trying to optimise your model by
+dnl using a value type narrower than "int32_t". In either case, you still do not
+dnl need to supply "size" if you never call the "*_size()" function; it is not
+dnl used internally within this template. If you call "*_size()" and your usage
+dnl falls into the (a) or (b) cases above, supply a "size" that is the number of
+dnl elements in "index_t" plus 1. Note that, e.g. if your indexing type is
+dnl "0..255", your size will need to be ≥ 256, preventing you using the value
+dnl type "uint8_t" which is not large enough to hold the value 256.
+dnl
+dnl This template is in the public domain. You may use it for any purpose and
+dnl its inclusion in a model does not affect the legal status of that model.
+dnl
+dnl ¹ https://en.wikipedia.org/wiki/M4_(computer_language)
+dnl
+define(`_list', `dnl
+-------------------------------------------------------------------------------
+-- interface for $1_t, a list of $3 values indexed by $2
+-------------------------------------------------------------------------------
+
+type
+  $1_t: array[$2] of record
+    -- Does this slot hold an item? The type 1..1 is used to model a boolean
+    -- without incurring an extra bit for the undefined value. I.e.
+    --   false = isundefined(is_populated_)
+    --   true = !isundefined(is_populated_)
+    is_populated_: 1..1;
+    -- the contents of the slot, if !isundefined(is_populated_)
+    value_: $3;
+  end;
+
+function $1_is_empty(list_: $1_t): boolean;
+begin
+  -- use a single-iteration loop to check the first element to avoid assuming
+  -- the lower bound of type $2
+  for i_: $2 do
+    if !isundefined(list_[i_].is_populated_) then
+      return false;
+    else
+      return true;
+    end;
+  end;
+  -- in the edge case where $2 is an empty type, consider the list always empty
+  return true;
+end;
+
+-- get the number of elements present in a list
+function $1_size(list_: $1_t): 0..ifelse(`$4', `', `2147483647', `$4');
+  var count_: 0..ifelse(`$4', `', `2147483647', `$4');
+begin
+  -- We have no easy way of checking the number of members in the type $2 at
+  -- generation time. So we use a runtime sanity check here that our return type
+  -- is large enough to represent the maximum size. A decent compiler will
+  -- constant fold and eliminate this in the common case where the type is
+  -- indeed large enough.
+  count_ := 0;
+  for i_: $2 do
+    assert
+      "0..ifelse(`$4', `', `2147483647', `$4') too small to represent $1_t size"
+      count_ < ifelse(`$4', `', `2147483647', `$4');
+    count_ := count_ + 1;
+  end;
+
+  count_ := 0;
+  for i_: $2 do
+    if !isundefined(list_[i_].is_populated_) then
+      count_ := count_ + 1;
+    end;
+  end;
+  return count_;
+end;
+
+function $1_is_full(list_: $1_t): boolean;
+begin
+  -- use a loop to check the last element to avoid assuming the upper bound of
+  -- type $2
+  for i_: $2 do
+    if isundefined(list_[i_].is_populated_) then
+      return false;
+    end;
+  end;
+  return true;
+end;
+
+-- Treating a $1_t as a first-in-first-out queue, enqueue an item. Or
+-- equivalently, treating a $1_t as a last-in-first-out stack, stack an item.
+procedure $1_push_back(var list_: $1_t; elem_: $3);
+begin
+  assert "attempting to push into a full $1_t" !$1_is_full(list_);
+  -- use a loop to find the first empty slot to avoid assuming the upper bound
+  -- of type $2
+  for i_: $2 do
+    if isundefined(list_[i_].is_populated_) then
+      list_[i_].value_ := elem_;
+      list_[i_].is_populated_ := 1;
+      return;
+    end;
+  end;
+  assert "unreachable code executed" false;
+end;
+
+-- Treating a $1_t as a first-in-first-out queue, enqueue an item and return
+-- true if possible. Or equivalently, treating a $1_t as a last-in-first-out
+-- stack, stack an item and return true if possible. If it is not possible to
+-- insert the new item, do nothing and return false.
+function $1_try_push_back(var list_: $1_t; elem_: $3): boolean;
+begin
+  if $1_is_full(list_) then
+    return false;
+  end;
+  $1_push_back(list_, elem_);
+  return true;
+end;
+
+-- treating a $1_t as a first-in-first-out queue, dequeue an item
+function $1_pop_front(var list_: $1_t): $3;
+var
+  first_: $3;
+  successor_: boolean;
+begin
+  assert "attempting to pop from an empty $1_t" !$1_is_empty(list_);
+  for i_: $2 do
+
+    -- extract the first element
+    assert "corrupted list" !isundefined(list_[i_].is_populated_);
+    first_ := list_[i_].value_;
+
+    -- Shuffle the remaining elements forwards. We do this with an unorthodox
+    -- double loop to avoid assuming anything about the bounds of $2 or
+    -- even whether its members are orderable.
+    for j_: $2 do
+      undefine list_[j_];
+      successor_ := false;
+      for k_: $2 do
+        if j_ = k_ then
+          assert "incorrect shuffle logic" !successor_;
+          successor_ := true;
+        elsif successor_ then
+          list_[j_] := list_[k_];
+          successor_ := false;
+        end;
+      end;
+    end;
+
+    return first_;
+  end;
+end;
+
+-- treating a $1_t as a last-in-first-out stack, unstack an item
+function $1_pop_back(var list_: $1_t): $3;
+var
+  last_: $3;
+  has_successor_: boolean;
+  successor_: boolean;
+begin
+  assert "attempting to pop from an empty $1_t" !$1_is_empty(list_);
+  for i_: $2 do
+
+    -- Is this element the last? We do this with an unorthodox loop to avoid
+    -- assuming anything about the bounds of $2 or even whether its members
+    -- are orderable.
+    has_successor_ := false;
+    for j_: $2 do
+      if i_ = j_ then
+        successor_ := true;
+      elsif successor_ then
+        has_successor_ := !isundefined(list_[j_].is_populated_);
+        successor_ := false;
+      end;
+    end;
+
+    -- if this is the last element, extract and return it
+    if !has_successor_ then
+      last_ := list_[i_].value_;
+      undefine list_[i_];
+      return last_;
+    end;
+  end;
+end;
+
+-------------------------------------------------------------------------------
+-- end interface for $1_t
+-------------------------------------------------------------------------------
+')dnl