13:0013:00, 6 January 2024diffhist+1,446 N
Monte Carlo Tree Search Game Play
Created page with "As of January 2024 ProB has a built-in algorithm for Monte Carlo Tree Search (MCTS). This can for example be used to perform game playing. In order to make use of MCTS one needs to provide information about the game state of a model by providing DEFINITIONS for: * GAME_OVER: must be TRUE when the game is finished; for a deadlock the game is also considered over (and by default drawn) * GAME_VALUE: must evaluate to a number if GAME_OVER is true. 0 is considered a draw, a..."
12:0012:00, 6 January 2024diffhist+235 N
Custom Graph
Created page with "You can visualise the state of an individual B, Z, TLA+ or Alloy model using custom graph definitions which are laid out using GraphViz. Thereby it is possible to specify general graph attributes, the nodes and the edges of the graph."
11:0611:06, 24 June 2022diffhist+1,434 N
Citing ProB
Created page with " The initial conference publication was: * Michael Leuschel & Michael Butler (2003): ProB: A Model Checker for B. In Keijiro Araki, Stefania Gnesi & Dino Mandrioli, editors:..."current
08:5308:53, 24 November 2021diffhist+1,299 N
Generating UML Sequence Charts
Created page with "= UML Sequence Charts for Traces ProB has a new experimental feature to generate a UML sequence chart from the current animation trace. It currently only works for classical..."
16:2516:25, 2 October 2021diffhist+679 N
Tips for Large Specifications
Created page with " If you have very large B machines, the following tips can be useful. Indeed, when you have very large B machines with hundreds of thousands or millions of lines of code, the..."
13:4513:45, 28 May 2021diffhist+553 N
Tutorial Tuning Model Checking
Created page with "Page is under construction == Reducing memory usage == You can try to reduce the memory consumption of ProB's model checker by setting the COMPRESSION preference to TRUE. Y..."
06:2706:27, 15 May 2021diffhist+751 N
Caching Constants and Operations
Created page with "ProB can store the values of constants and operations in a cache file. Compared to [Memoization_for_Functions|memoization for functions], this caching is persistant across dif..."
08:5308:53, 24 March 2021diffhist+704 N
Reals and Floats
Created page with "ProB now supports the Atelier-B datatypes REAL and FLOAT. You can turn off this support via the preference ALLOW_REALS. Standard arithmetic operators can be applied to reals..."
