B2SAT - Revision history

Michael Leuschel: /* B2SAT for TLA+, Z and Alloy */

2024-04-24T12:13:13Z

B2SAT for TLA+, Z and Alloy

← Older revision		Revision as of 12:13, 24 April 2024
Line 143:		Line 143:
	Below is the dominating set example from above as a TLA+ machine that can be loaded and solved by ProB.		Below is the dominating set example from above as a TLA+ machine that can be loaded and solved by ProB.
	The custom graph visualisation derived from CUSTOM_GRAPH is also similar.		The custom graph visualisation derived from CUSTOM_GRAPH is also similar.

			The model cannot be run with TLC nor with Apalache as neither tool can find constants that satisfy the assumptions (Apalache reports: "The following CONSTANTS are not initialized: ice").

	<pre>		<pre>

Michael Leuschel: /* B2SAT for TLA+, Z and Alloy */

2024-04-24T10:59:12Z

B2SAT for TLA+, Z and Alloy

@@ Line 177: / Line 177: @@
               edges |-> edge]]
 ====
 </pre>

Michael Leuschel at 10:57, 24 April 2024

2024-04-24T10:57:58Z

← Older revision		Revision as of 10:57, 24 April 2024
Line 136:		Line 136:

	[[File:JupypterOpt3.png\|700px\|center]]		[[File:JupypterOpt3.png\|700px\|center]]

			= B2SAT for TLA+, Z and Alloy =

			B2SAT is also available for other state-based languages supported by ProB.

			Below is the dominating set example from above as a TLA+ machine that can be loaded and solved by ProB.
			The custom graph visualisation derived from CUSTOM_GRAPH is also similar.

			<pre>
			---- MODULE IceCream_Generic_cst ----
			EXTENDS Naturals, FiniteSets
			CONSTANTS n1, n2, n3, n4, n5, n6, n7, n8, n9, n10,
			n11, n12, n13, n14, n15, n16, n17, n18, n19, n20,
			n21, n22, n23, n24,
			ice
			VARIABLES vans
			NODES == {n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, n12, n13, n14, n15, n16, n17, n18, n19, n20, n21, n22, n23, n24}

			SET_PREF_TIME_OUT == 1500
			SET_PREF_SOLVER_FOR_PROPERTIES == "sat"

			edge == {<<n1, n2>>, <<n1, n4>>, <<n2, n3>>, <<n3, n4>>, <<n3, n5>>, <<n3, n7>>, <<n4, n7>>, <<n5, n6>>, <<n5, n9>>, <<n6, n7>>, <<n6, n8>>, <<n7, n8>>, <<n8, n10>>, <<n8, n13>>, <<n9, n10>>, <<n9, n11>>, <<n9, n12>>, <<n11, n12>>, <<n11, n14>>, <<n12, n13>>, <<n13, n16>>, <<n14, n15>>, <<n14, n17>>, <<n15, n16>>, <<n15, n17>>, <<n15, n18>>, <<n15, n21>>, <<n16, n18>>, <<n16, n19>>, <<n17, n19>>, <<n18, n19>>, <<n18, n20>>, <<n18, n21>>, <<n19, n20>>, <<n19, n21>>, <<n20, n21>>, <<n20, n22>>, <<n21, n22>>, <<n21, n23>>, <<n21, n24>>, <<n22, n23>>, <<n21, n24>>, <<n23, n24>>}

			DomSet == (\A x \in NODES : (ice[x] = TRUE \/ (\E nbour \in NODES : (<<nbour,x>> \in edge \/ <<x,nbour>> \in edge) /\ ice[nbour] = TRUE)))

			ASSUME ice \in [NODES -> BOOLEAN] /\ DomSet /\ Cardinality({x \in (NODES): ice[x] = TRUE}) =< 6

			Init ==
			vans = Cardinality({x\in NODES : ice[x]=TRUE})

			Invariant ==
			vans \in (0 .. 10)

			Next == UNCHANGED <<ice, vans>>

			CUSTOM_GRAPH == [layout \|-> "dot", rankdir \|-> "TB",
			nodes \|-> {[value \|-> j, style \|-> "filled",
			fillcolor \|-> (IF ice[j] = TRUE THEN "mistyrose" ELSE "white")]: j \in NODES},
			edges \|-> [color \|-> "gray", arrowhead \|-> "odot", arrowtail \|-> "odot", dir \|-> "both", label \|-> "edge",
			edges \|-> edge]]
			====
			</pre>

Michael Leuschel: /* B2SAT in the REPL */

2024-04-24T07:41:09Z

B2SAT in the REPL

← Older revision		Revision as of 07:41, 24 April 2024
Line 22:		Line 22:
	=== B2SAT in the REPL ===		=== B2SAT in the REPL ===

	The following four commands are now available in REPL of probcli (start with <tt>probcli --repl</tt>):		The following four commands are now available in REPL of [[Using_the_Command-Line_Version_of_ProB\|probcli]] (start with <tt>probcli --repl</tt>):
	* :sat PRED		* :sat PRED
	* :sat-z3 PRED		* :sat-z3 PRED

Michael Leuschel: /* B2SAT in Jupyter Notebooks */

2024-04-24T07:40:33Z

B2SAT in Jupyter Notebooks

← Older revision		Revision as of 07:40, 24 April 2024
Line 121:		Line 121:
	=== B2SAT in Jupyter Notebooks ===		=== B2SAT in Jupyter Notebooks ===

	The solve command in the https://gitlab.cs.uni-duesseldorf.de/general/stups/prob2-jupyter-kernel ProB Jupyter kernel now supports <tt>sat</tt> and <tt>satz3</tt> as solvers.		The solve command in the [https://gitlab.cs.uni-duesseldorf.de/general/stups/prob2-jupyter-kernel ProB Jupyter kernel] now supports <tt>sat</tt> and <tt>satz3</tt> as solvers.
	They use B2SAT with Glucose and Z3 as SAT solvers respectively.		They use B2SAT with Glucose and Z3 as SAT solvers respectively.

Michael Leuschel: /* B2SAT in Jupyter Notebooks */

2024-04-24T07:40:15Z

B2SAT in Jupyter Notebooks

← Older revision		Revision as of 07:40, 24 April 2024
Line 121:		Line 121:
	=== B2SAT in Jupyter Notebooks ===		=== B2SAT in Jupyter Notebooks ===

	The solve command in the ProB Jupyter kernel now supports <tt>sat</tt> and <tt>satz3</tt> as solvers.		The solve command in the https://gitlab.cs.uni-duesseldorf.de/general/stups/prob2-jupyter-kernel ProB Jupyter kernel now supports <tt>sat</tt> and <tt>satz3</tt> as solvers.
	They use B2SAT with Glucose and Z3 as SAT solvers respectively.		They use B2SAT with Glucose and Z3 as SAT solvers respectively.

Michael Leuschel at 07:38, 24 April 2024

2024-04-24T07:38:56Z

← Older revision		Revision as of 07:38, 24 April 2024
Line 115:		Line 115:
	By choosing "Show Source Code Coverage" in the Debug menu of ProB Tcl/Tk you can see which parts of the properties were translated to SAT (in green) and which were processed entirely by ProB (in red-orange):		By choosing "Show Source Code Coverage" in the Debug menu of ProB Tcl/Tk you can see which parts of the properties were translated to SAT (in green) and which were processed entirely by ProB (in red-orange):

	[[File:IceCreamCoverage.png\|~~700px~~\|center]]		[[File:IceCreamCoverage.png\|600px\|center]]

	On the console you can also see feedback about which parts were translated and which ones not.		On the console you can also see feedback about which parts were translated and which ones not.

Michael Leuschel at 07:38, 24 April 2024

2024-04-24T07:38:29Z

← Older revision		Revision as of 07:38, 24 April 2024
Line 16:		Line 16:
	* propagation of the SAT solution to B, by progressively grounding the B values and predicates linked to the propositional variables.		* propagation of the SAT solution to B, by progressively grounding the B values and predicates linked to the propositional variables.
	* complete constraint solving, solving the pending constraints in B by now performing the regular non-deterministic propagations and enumerations of ProB.		* complete constraint solving, solving the pending constraints in B by now performing the regular non-deterministic propagations and enumerations of ProB.


	~~[[File:IceCreamCoverage.png\|700px\|center]]~~


Line 42:		Line 39:
	=== B2SAT for PROPERTIES ===		=== B2SAT for PROPERTIES ===

	The new preference SOLVER_FOR_PROPERTIES can be used to specify solver for PROPERTIES (axioms) when setting up constants.		The new preference <tt>SOLVER_FOR_PROPERTIES</tt> can be used to specify solver for PROPERTIES (axioms) when setting up constants.
	The valid settings are: prob (the default), kodkod, z3, z3cns, z3axm, cdclt, sat, sat-z3.		The valid settings are: prob (the default), kodkod, z3, z3cns, z3axm, cdclt, sat, sat-z3.

	The last two will use B2SAT, <tt>sat</tt> with Glucose as SAT solver and <tt>sat-z3</tt> with Z3 as SAT solver.		The last two will use B2SAT, <tt>sat</tt> with Glucose as SAT solver and <tt>sat-z3</tt> with Z3 as SAT solver.

	Here is an example using this preference:		Here is an example using this preference to compute a dominating set of a graph:

	<pre>		<pre>
	MACHINE IceCream_Generic		MACHINE IceCream_Generic
	// Dominating set example:		// Dominating set example:
	// place ice cream vans so that every house (node) is at most one block away from a van		// place ice cream vans so that every house (node) is at most one block away from a van
	~~// a version which can be solved by B2SAT~~
	DEFINITIONS		DEFINITIONS
	N == 24;		N == 24;
	CUSTOM_GRAPH == rec(layout:"dot", rankdir:"TB",		CUSTOM_GRAPH == rec(layout:"dot", rankdir:"TB",
	nodes: {j•j:NODES \|		nodes: {j•j:NODES \|
	rec(value:j, style:"filled",		rec(value:j, style:"filled",
Line 65:		Line 62:
	);		);
	bi_edge == (edge \/ edge~);		bi_edge == (edge \/ edge~);
	~~SET_PREF_SMT == TRUE;~~
	~~SET_PREF_TIME_OUT == 50000;~~
	~~SET_PREF_SOLVER_STRENGTH == 300;~~
	SET_PREF_SOLVER_FOR_PROPERTIES == "sat";		SET_PREF_SOLVER_FOR_PROPERTIES == "sat";
	SETS		SETS

Michael Leuschel at 07:35, 24 April 2024

2024-04-24T07:35:18Z

← Older revision		Revision as of 07:35, 24 April 2024
Line 17:		Line 17:
	* complete constraint solving, solving the pending constraints in B by now performing the regular non-deterministic propagations and enumerations of ProB.		* complete constraint solving, solving the pending constraints in B by now performing the regular non-deterministic propagations and enumerations of ProB.


			[[File:IceCreamCoverage.png\|700px\|center]]

Michael Leuschel: /* B2SAT for PROPERTIES */

2024-04-24T07:34:50Z

B2SAT for PROPERTIES

← Older revision		Revision as of 07:34, 24 April 2024
Line 114:		Line 114:
	Here is the graphical rendering of a solution using the custom graph definition above:		Here is the graphical rendering of a solution using the custom graph definition above:

	[[File:IceCream_Generic.png\|~~700px~~\|center]]		[[File:IceCream_Generic.png\|500px\|center]]


	By choosing "Show Source Code Coverage" in the Debug menu of ProB Tcl/Tk you can see which parts of the properties were translated to SAT (in green) and which were processed entirely by ProB (in red-orange):		By choosing "Show Source Code Coverage" in the Debug menu of ProB Tcl/Tk you can see which parts of the properties were translated to SAT (in green) and which were processed entirely by ProB (in red-orange):


	~~Here is the graphical rendering of a solution using the custom graph definition above:~~

	[[File:IceCreamCoverage.png\|700px\|center]]		[[File:IceCreamCoverage.png\|700px\|center]]