markuzzz
markuzzz
Using the latest nightly build I consistently get a bus error for the attached model, but only if the number of threads is set to more than one. Steps to...
Lpsxsim crashes when selecting a specific transition. Tool version: latest nightly build for Mac OS (202106.0.d775157140) Can be reproduced by taking two transitions in the LPS using lpsxsim. selectMultiStep(none, StateConfig(F_P3_SR_STD_1,...
In equations it is possible to use the construction **whr** z = x + y **end**. This is a very convenient way of using shorthands in complex data expressions. In...
Suppose we have ``` map test: List(Int) -> Int; var ls: List(Int); i: Int; ``` Then the equation `test(i |> ls) = i` is fine. `test[i]` will be rewritten to...
The documentation does not state that lps2pbes can be used to only check a formula: https://mcrl2.org/web/user_manual/tools/release/lps2pbes.html But running "lps2pbes .lps .mcf --check-only" does actually work. It nicely prints whether the...
Recently during a training we discovered that ltsgraph and ltsview were not working properly on the machines of most of the participants. With ltsgraph they got a blank white window...
It is a common use case to use 'observation variables' in mu-calculus formulas to track the state of the system. Certain action then change these variables, usually only one at...