ProB Logic Calculator - Revision history

Michael Leuschel at 11:47, 8 November 2022

2022-11-08T11:47:38Z

← Older revision		Revision as of 11:47, 8 November 2022
Line 48:		Line 48:
	* support for further alternative input syntax, such as [http://en.wikipedia.org/wiki/Z_notation Z]		* support for further alternative input syntax, such as [http://en.wikipedia.org/wiki/Z_notation Z]
	* ability to change the parameters, e.g., use the [http://www.stups.uni-duesseldorf.de/w/Special:Publication/PlaggeLeuschel_Kodkod2012 ProB-Kodkod backend] instead of the default constraint-logic programming kernel.		* ability to change the parameters, e.g., use the [http://www.stups.uni-duesseldorf.de/w/Special:Publication/PlaggeLeuschel_Kodkod2012 ProB-Kodkod backend] instead of the default constraint-logic programming kernel.

			Its code is available at <tt>https://github.com/bendisposto/evalB</tt>.

	== Small Tutorial ==		== Small Tutorial ==
Line 118:		Line 120:
	Probably, you may want to generate full-fledged B machines as input to <tt>probcli</tt>.		Probably, you may want to generate full-fledged B machines as input to <tt>probcli</tt>.
	This allows you to introduce enumerated and deferred sets; compared to using sets of strings, this has benefits in terms of more stringent typechecking and more efficient constraint solving.		This allows you to introduce enumerated and deferred sets; compared to using sets of strings, this has benefits in terms of more stringent typechecking and more efficient constraint solving.

	~~Its code is available at <tt>https://github.com/bendisposto/evalB</tt>.~~

Michael Leuschel: /* Executing the Calculator locally */

2022-11-08T11:46:53Z

Executing the Calculator locally

← Older revision		Revision as of 11:46, 8 November 2022
Line 98:		Line 98:

	== Executing the Calculator locally ==		== Executing the Calculator locally ==

			You can evaluate formulas on your machine in the same way as the calculator above, by [[Download\|downloading ProB]] (ideally a nightly build) and then executing, e.g., this
			command:
			./probcli -repl -p BOOL_AS_PREDICATE TRUE -p MAXINT 127 -p MININT -128
			You can of course adapt the preferences (TIME_OUT, MININT, MAXINT, ...) according to your needs; the [[Using_the_Command-Line_Version_of_ProB\|user manual]] provides more details.
			You may wish to use the rlwrap tool:
			rlwrap ./probcli -repl -p BOOL_AS_PREDICATE TRUE -p CLPFD TRUE -p MAXINT 127 -p MININT -128

	[[file:ProBTerminalizerReplDemo.gif\|center\|\|600px]]		[[file:ProBTerminalizerReplDemo.gif\|center\|\|600px]]

	You can evaluate formulas ~~on your machine~~ in ~~the same way as the calculator above,~~ by ~~[[Download\|downloading ProB]] (ideally a nightly build) and then~~ executing one of the following commands:		You can also evaluate formulas in batch mode by executing one of the following commands:
	./probcli -p BOOL_AS_PREDICATE TRUE -p MAXINT 127 -p MININT -128 -p TIME_OUT 500 -eval_file MYFILE		./probcli -p BOOL_AS_PREDICATE TRUE -p MAXINT 127 -p MININT -128 -p TIME_OUT 500 -eval_file MYFILE
	The above command requires you to put the formula into a file <tt>MYFILE</tt>.		The above command requires you to put the formula into a file <tt>MYFILE</tt>.
Line 108:		Line 115:
	If you want to perform the tautology check you have to do the following using the -eval_rule_file command:		If you want to perform the tautology check you have to do the following using the -eval_rule_file command:
	./probcli -p BOOL_AS_PREDICATE TRUE -p MAXINT 127 -p MININT -128 -p TIME_OUT 500 -eval_rule_file MYFILE		./probcli -p BOOL_AS_PREDICATE TRUE -p MAXINT 127 -p MININT -128 -p TIME_OUT 500 -eval_rule_file MYFILE

	~~You can also start your own REPL using the -repl command:~~
	~~./probcli -repl -p BOOL_AS_PREDICATE TRUE -p MAXINT 127 -p MININT -128~~
	~~You can of course adapt the preferences (TIME_OUT, MININT, MAXINT, ...) according to your needs; the [[Using_the_Command-Line_Version_of_ProB\|user manual]] provides more details.~~
	~~You may wish to use the rlwrap tool:~~
	~~rlwrap ./probcli -repl -p BOOL_AS_PREDICATE TRUE -p CLPFD TRUE -p MAXINT 127 -p MININT -128~~

	Probably, you may want to generate full-fledged B machines as input to <tt>probcli</tt>.		Probably, you may want to generate full-fledged B machines as input to <tt>probcli</tt>.

Michael Leuschel: /* Executing the Calculator locally */

2022-11-08T11:43:52Z

Executing the Calculator locally

Michael Leuschel at 14:29, 17 October 2022

2022-10-17T14:29:50Z

← Older revision		Revision as of 14:29, 17 October 2022
Line 1:		Line 1:
	Below is a ProB-based logic calculator. You can enter predicates and expressions in the upper textfield ([[Summary_of_B_Syntax\|using B syntax]]). When you stop typing, ProB will evaluate the formula and display the result in the lower textfield. A series of examples for the "Evaluate" mode can be loaded from the examples menu. There is a [[ProB_Logic_Calculator#Small_Tutorial\|small tutorial]] at the bottom of the page.		Below is a ProB-based logic calculator. You can enter predicates and expressions in the upper textfield ([[Summary_of_B_Syntax\|using B syntax]]). When you stop typing, ProB will evaluate the formula and display the result in the lower textfield. A series of examples for the "Evaluate" mode can be loaded from the examples menu. There is a [[ProB_Logic_Calculator#Small_Tutorial\|small tutorial]] at the bottom of the page.

	[[Image:EvalB.png\|600px \|link=~~http~~://eval-b.stups.~~uni-duesseldorf~~.de]]		[[Image:EvalB.png\|600px \|link=https://eval-b.stups.hhu.de]]

	<!--		<!--
	Does not work in Safari/... on Mac as http in https does not work		Does not work in Safari/... on Mac as http in https does not work
	<html>		<html>
	<iframe src="~~http~~://eval-b.stups.~~uni-duesseldorf~~.de~~/embedded.html~~" width="780" height="450" border="0" frameborder="0" scrolling="no">		<iframe src="https://eval-b.stups.hhu.de" width="780" height="450" border="0" frameborder="0" scrolling="no">
	<p>Your Browser does not suport IFrames.</p>		<p>Your Browser does not suport IFrames.</p>
	</iframe>		</iframe>

Michael Leuschel at 14:29, 17 October 2022

2022-10-17T14:29:11Z

← Older revision		Revision as of 14:29, 17 October 2022
Line 12:		Line 12:
	-->		-->

	[~~http~~://eval-b.stups.~~uni-duesseldorf~~.de/ Start ProB Logic Calculator].		[https://eval-b.stups.hhu.de Start ProB Logic Calculator].

	The above calculator has a time-out of 3 seconds, and <tt>MAXINT</tt> is set to 127 and <tt>MININT</tt> to -128.		The above calculator has a time-out of 3 seconds, and <tt>MAXINT</tt> is set to 127 and <tt>MININT</tt> to -128.

Michael Leuschel at 16:21, 13 January 2022

2022-01-13T16:21:07Z

← Older revision		Revision as of 16:21, 13 January 2022
Line 1:		Line 1:
	Below is a ProB-based ~~[http://research.microsoft.com/en-us/um/people/lamport/tla/logic-calculators.html~~ logic calculator]. You can enter predicates and expressions in the upper textfield ([[Summary_of_B_Syntax\|using B syntax]]). When you stop typing, ProB will evaluate the formula and display the result in the lower textfield. A series of examples for the "Evaluate" mode can be loaded from the examples menu. There is a [[ProB_Logic_Calculator#Small_Tutorial\|small tutorial]] at the bottom of the page.		Below is a ProB-based logic calculator. You can enter predicates and expressions in the upper textfield ([[Summary_of_B_Syntax\|using B syntax]]). When you stop typing, ProB will evaluate the formula and display the result in the lower textfield. A series of examples for the "Evaluate" mode can be loaded from the examples menu. There is a [[ProB_Logic_Calculator#Small_Tutorial\|small tutorial]] at the bottom of the page.

	[[Image:EvalB.png\|600px \|link=http://eval-b.stups.uni-duesseldorf.de]]		[[Image:EvalB.png\|600px \|link=http://eval-b.stups.uni-duesseldorf.de]]

Jens Bendisposto at 12:47, 13 February 2020

2020-02-13T12:47:52Z

← Older revision		Revision as of 12:47, 13 February 2020
Line 1:		Line 1:
	Below is a ProB-based [http://research.microsoft.com/en-us/um/people/lamport/tla/logic-calculators.html logic calculator]. You can enter predicates and expressions in the upper textfield ([[Summary_of_B_Syntax\|using B syntax]]). When you stop typing, ProB will evaluate the formula and display the result in the lower textfield. A series of examples for the "Evaluate" mode can be loaded from the examples menu. There is a [[ProB_Logic_Calculator#Small_Tutorial\|small tutorial]] at the bottom of the page.		Below is a ProB-based [http://research.microsoft.com/en-us/um/people/lamport/tla/logic-calculators.html logic calculator]. You can enter predicates and expressions in the upper textfield ([[Summary_of_B_Syntax\|using B syntax]]). When you stop typing, ProB will evaluate the formula and display the result in the lower textfield. A series of examples for the "Evaluate" mode can be loaded from the examples menu. There is a [[ProB_Logic_Calculator#Small_Tutorial\|small tutorial]] at the bottom of the page.

	[[Image:EvalB.png\|600px \|link=http://eval-b.stups.uni-duesseldorf.de]		[[Image:EvalB.png\|600px \|link=http://eval-b.stups.uni-duesseldorf.de]]

	<!--		<!--

Jens Bendisposto at 12:47, 13 February 2020

2020-02-13T12:47:28Z

← Older revision		Revision as of 12:47, 13 February 2020
Line 1:		Line 1:
	Below is a ProB-based [http://research.microsoft.com/en-us/um/people/lamport/tla/logic-calculators.html logic calculator]. You can enter predicates and expressions in the upper textfield ([[Summary_of_B_Syntax\|using B syntax]]). When you stop typing, ProB will evaluate the formula and display the result in the lower textfield. A series of examples for the "Evaluate" mode can be loaded from the examples menu. There is a [[ProB_Logic_Calculator#Small_Tutorial\|small tutorial]] at the bottom of the page.		Below is a ProB-based [http://research.microsoft.com/en-us/um/people/lamport/tla/logic-calculators.html logic calculator]. You can enter predicates and expressions in the upper textfield ([[Summary_of_B_Syntax\|using B syntax]]). When you stop typing, ProB will evaluate the formula and display the result in the lower textfield. A series of examples for the "Evaluate" mode can be loaded from the examples menu. There is a [[ProB_Logic_Calculator#Small_Tutorial\|small tutorial]] at the bottom of the page.

	[[Image:EvalB.png\|600px \|link=http://eval-b.stups.uni-duesseldorf.de/]		[[Image:EvalB.png\|600px \|link=http://eval-b.stups.uni-duesseldorf.de]

	<!--		<!--

Jens Bendisposto at 12:46, 13 February 2020

2020-02-13T12:46:53Z

← Older revision		Revision as of 12:46, 13 February 2020
Line 1:		Line 1:
	Below is a ProB-based [http://research.microsoft.com/en-us/um/people/lamport/tla/logic-calculators.html logic calculator]. You can enter predicates and expressions in the upper textfield ([[Summary_of_B_Syntax\|using B syntax]]). When you stop typing, ProB will evaluate the formula and display the result in the lower textfield. A series of examples for the "Evaluate" mode can be loaded from the examples menu. There is a [[ProB_Logic_Calculator#Small_Tutorial\|small tutorial]] at the bottom of the page.		Below is a ProB-based [http://research.microsoft.com/en-us/um/people/lamport/tla/logic-calculators.html logic calculator]. You can enter predicates and expressions in the upper textfield ([[Summary_of_B_Syntax\|using B syntax]]). When you stop typing, ProB will evaluate the formula and display the result in the lower textfield. A series of examples for the "Evaluate" mode can be loaded from the examples menu. There is a [[ProB_Logic_Calculator#Small_Tutorial\|small tutorial]] at the bottom of the page.

	[[Image:EvalB.png\|600px \|link=http://~~wyvern~~.cs.uni-duesseldorf.de~~:8443~~/~~index.html]~~]		[[Image:EvalB.png\|600px \|link=http://eval-b.stups.uni-duesseldorf.de/]

	<!--		<!--
	Does not work in Safari/... on Mac as http in https does not work		Does not work in Safari/... on Mac as http in https does not work
	<html>		<html>
	<iframe src="http://~~wyvern~~.cs.uni-duesseldorf.de~~:8443~~/embedded.html" width="780" height="450" border="0" frameborder="0" scrolling="no">		<iframe src="http://eval-b.stups.uni-duesseldorf.de/embedded.html" width="780" height="450" border="0" frameborder="0" scrolling="no">
	<p>Your Browser does not suport IFrames.</p>		<p>Your Browser does not suport IFrames.</p>
	</iframe>		</iframe>
Line 12:		Line 12:
	-->		-->

	[http://~~wyvern~~.cs.uni-duesseldorf.de~~:8443~~/~~index.html~~ Start ProB Logic Calculator].		[http://eval-b.stups.uni-duesseldorf.de/ Start ProB Logic Calculator].

	The above calculator has a time-out of 3 seconds, and <tt>MAXINT</tt> is set to 127 and <tt>MININT</tt> to -128.		The above calculator has a time-out of 3 seconds, and <tt>MAXINT</tt> is set to 127 and <tt>MININT</tt> to -128.
Line 114:		Line 114:
	This allows you to introduce enumerated and deferred sets; compared to using sets of strings, this has benefits in terms of more stringent typechecking and more efficient constraint solving.		This allows you to introduce enumerated and deferred sets; compared to using sets of strings, this has benefits in terms of more stringent typechecking and more efficient constraint solving.

	~~An alternate front-end to the calculator is [http://wyvern.cs.uni-duesseldorf.de:8443/ available here].~~
	Its code is available at <tt>https://github.com/bendisposto/evalB</tt>.		Its code is available at <tt>https://github.com/bendisposto/evalB</tt>.

Jens Bendisposto at 07:53, 6 October 2017

2017-10-06T07:53:15Z

← Older revision		Revision as of 07:53, 6 October 2017
Line 1:		Line 1:
	Below is a ProB-based [http://research.microsoft.com/en-us/um/people/lamport/tla/logic-calculators.html logic calculator]. You can enter predicates and expressions in the upper textfield ([[Summary_of_B_Syntax\|using B syntax]]). When you stop typing, ProB will evaluate the formula and display the result in the lower textfield. A series of examples for the "Evaluate" mode can be loaded from the examples menu. There is a [[ProB_Logic_Calculator#Small_Tutorial\|small tutorial]] at the bottom of the page.		Below is a ProB-based [http://research.microsoft.com/en-us/um/people/lamport/tla/logic-calculators.html logic calculator]. You can enter predicates and expressions in the upper textfield ([[Summary_of_B_Syntax\|using B syntax]]). When you stop typing, ProB will evaluate the formula and display the result in the lower textfield. A series of examples for the "Evaluate" mode can be loaded from the examples menu. There is a [[ProB_Logic_Calculator#Small_Tutorial\|small tutorial]] at the bottom of the page.

			[[Image:EvalB.png\|600px \|link=http://wyvern.cs.uni-duesseldorf.de:8443/index.html]]
	[http://wyvern.cs.uni-duesseldorf.de:8443/index.html ~~[[File:EvalB.png\|600px]~~]]

	<!--		<!--

← Older revision		Revision as of 11:43, 8 November 2022
Line 98:		Line 98:

	== Executing the Calculator locally ==		== Executing the Calculator locally ==

			[[file:ProBTerminalizerReplDemo.gif\|center\|\|600px]]

	You can evaluate formulas on your machine in the same way as the calculator above, by [[Download\|downloading ProB]] (ideally a nightly build) and then executing one of the following commands:		You can evaluate formulas on your machine in the same way as the calculator above, by [[Download\|downloading ProB]] (ideally a nightly build) and then executing one of the following commands:
	./probcli -p BOOL_AS_PREDICATE ~~TRUE -p CLPFD~~ TRUE -p MAXINT 127 -p MININT -128 -p TIME_OUT 500 -eval_file MYFILE		./probcli -p BOOL_AS_PREDICATE TRUE -p MAXINT 127 -p MININT -128 -p TIME_OUT 500 -eval_file MYFILE
	The above command requires you to put the formula into a file <tt>MYFILE</tt>.		The above command requires you to put the formula into a file <tt>MYFILE</tt>.
	The command below allows you to put the formula directly into the command:		The command below allows you to put the formula directly into the command:
	./probcli -p BOOL_AS_PREDICATE ~~TRUE -p CLPFD~~ TRUE -p MAXINT 127 -p MININT -128 -p TIME_OUT 500 -eval "MYFORMULA"		./probcli -p BOOL_AS_PREDICATE TRUE -p MAXINT 127 -p MININT -128 -p TIME_OUT 500 -eval "MYFORMULA"
	If you want to perform the tautology check you have to do the following using the -eval_rule_file command:		If you want to perform the tautology check you have to do the following using the -eval_rule_file command:
	./probcli -p BOOL_AS_PREDICATE ~~TRUE -p CLPFD~~ TRUE -p MAXINT 127 -p MININT -128 -p TIME_OUT 500 -eval_rule_file MYFILE		./probcli -p BOOL_AS_PREDICATE TRUE -p MAXINT 127 -p MININT -128 -p TIME_OUT 500 -eval_rule_file MYFILE
	You can also start your own REPL using the -repl command ~~(you may wish to use the rlwrap tool)~~:
	./probcli -repl -p BOOL_AS_PREDICATE ~~TRUE -p CLPFD~~ TRUE -p MAXINT 127 -p MININT -128		You can also start your own REPL using the -repl command:
			./probcli -repl -p BOOL_AS_PREDICATE TRUE -p MAXINT 127 -p MININT -128
	You can of course adapt the preferences (TIME_OUT, MININT, MAXINT, ...) according to your needs; the [[Using_the_Command-Line_Version_of_ProB\|user manual]] provides more details.		You can of course adapt the preferences (TIME_OUT, MININT, MAXINT, ...) according to your needs; the [[Using_the_Command-Line_Version_of_ProB\|user manual]] provides more details.
	You may wish to use the rlwrap tool:		You may wish to use the rlwrap tool: