Generating Documents with ProB and Latex - Revision history

Michael Leuschel: /* Some Examples */

2016-10-25T05:57:27Z

Some Examples

← Older revision		Revision as of 05:57, 25 October 2016
Line 54:		Line 54:

	* Presentation held in Grenoble in September 2016 about "Constraint Programming Puzzles in B" [[File:puzzle_latex_presentation.pdf]]		* Presentation held in Grenoble in September 2016 about "Constraint Programming Puzzles in B" [[File:puzzle_latex_presentation.pdf]]


	* SBMF'2016 keynote article "Formal Model-Based Constraint Solving and Document Generation" [[File:sbmf_2016_latex.pdf]]		* SBMF'2016 keynote article "Formal Model-Based Constraint Solving and Document Generation" [[File:sbmf_2016_latex.pdf]]

Michael Leuschel: /* Some Examples */

2016-10-25T05:54:28Z

Some Examples

← Older revision		Revision as of 05:54, 25 October 2016
Line 53:		Line 53:
	== Some Examples ==		== Some Examples ==

	* Presentation held in Grenoble in September 2016 about "Constraint Programming Puzzles in B" [[File:puzzle_latex_presentation.pdf ~~slides as PDF~~]]		* Presentation held in Grenoble in September 2016 about "Constraint Programming Puzzles in B" [[File:puzzle_latex_presentation.pdf]]


	* SBMF'2016 keynote article "Formal Model-Based Constraint Solving and Document Generation" [[File:sbmf_2016_latex.pdf ~~slides as PDF~~]]		* SBMF'2016 keynote article "Formal Model-Based Constraint Solving and Document Generation" [[File:sbmf_2016_latex.pdf]]

Michael Leuschel: /* Some Examples */

2016-10-25T05:52:20Z

Some Examples

← Older revision		Revision as of 05:52, 25 October 2016
Line 53:		Line 53:
	== Some Examples ==		== Some Examples ==

	* Presentation held in Grenoble in September 2016 about "Constraint Programming Puzzles in B" [[File:~~puzzle_presentation~~.pdf slides as PDF]]		* Presentation held in Grenoble in September 2016 about "Constraint Programming Puzzles in B" [[File:puzzle_latex_presentation.pdf slides as PDF]]


			* SBMF'2016 keynote article "Formal Model-Based Constraint Solving and Document Generation" [[File:sbmf_2016_latex.pdf slides as PDF]]

Michael Leuschel: /* Some Examples */

2016-10-25T05:50:24Z

Some Examples

← Older revision		Revision as of 05:50, 25 October 2016
Line 53:		Line 53:
	== Some Examples ==		== Some Examples ==

	* Presentation held in Grenoble in September 2016 about "Constraint Programming Puzzles in B"		* Presentation held in Grenoble in September 2016 about "Constraint Programming Puzzles in B" [[File:puzzle_presentation.pdf slides as PDF]]
	[[File:puzzle_presentation.pdf slides as PDF]]

Michael Leuschel at 05:50, 25 October 2016

2016-10-25T05:50:03Z

← Older revision		Revision as of 05:50, 25 October 2016
Line 50:		Line 50:

	* <tt>\probfor{ID}{Set}{Body}</tt> command takes an identifier <tt>ID</tt>, a set expression <tt>Set</tt> and a Latex text <tt>Body</tt>, and processes the Latex text for every element of the set expression, setting the identifier to a value of the set.		* <tt>\probfor{ID}{Set}{Body}</tt> command takes an identifier <tt>ID</tt>, a set expression <tt>Set</tt> and a Latex text <tt>Body</tt>, and processes the Latex text for every element of the set expression, setting the identifier to a value of the set.

			== Some Examples ==

			* Presentation held in Grenoble in September 2016 about "Constraint Programming Puzzles in B"
			[[File:puzzle_presentation.pdf slides as PDF]]

Michael Leuschel: /* Commands */

2016-09-07T11:36:03Z

Commands

← Older revision		Revision as of 11:36, 7 September 2016
Line 25:		Line 25:
	Here is a short summary of some of the commands:		Here is a short summary of some of the commands:
	* <tt>\probexpr{EXRP}</tt> command takes a B expression <tt>EXPR</tt>as argument and evaluates it. By default it shows the B expression and the value of the expression. Example: <tt>\probexpr{{1}\/{2**10}}</tt> will be replaced by <tt>{1,1024}</tt>		* <tt>\probexpr{EXRP}</tt> command takes a B expression <tt>EXPR</tt>as argument and evaluates it. By default it shows the B expression and the value of the expression. Example: <tt>\probexpr{{1}\/{2**10}}</tt> will be replaced by <tt>{1,1024}</tt>
			** <tt>ascii</tt> to print the result as ASCII rather than using Latex math symbols
			** <tt>time</tt> to display the time taken for the command
			** <tt>string</tt> the result value is a string, and do not print the quotes around the string
			** <tt>value</tt> to just print the value, not the expression

	* <tt>\probrepl{CMD}</tt> command takes a probcli REPL command <tt>CMD</tt> as argument and executes it. By default it shows only the output of the execution, e.g., in case it is a predicate TRUE or FALSE. Example: <tt>\probrepl{let DOM = 1..3}</tt>. A variation of the latter is the new command <tt>\problet{DOM}{1..3}</tt> which shows the let construct itself within the generated Latex. Optional arguments for <tt>\~~probrep~~<\tt> are :		* <tt>\probrepl{CMD}</tt> command takes a probcli REPL command <tt>CMD</tt> as argument and executes it. By default it shows only the output of the execution, e.g., in case it is a predicate TRUE or FALSE. Example: <tt>\probrepl{let DOM = 1..3}</tt>. A variation of the latter is the new command <tt>\problet{DOM}{1..3}</tt> which shows the let construct itself within the generated Latex. Optional arguments for <tt>\probrepl</tt> are :
	**<tt>solution</tt> to display the solution bindings (for existential variables) found by ProB		**<tt>solution</tt> to display the solution bindings (for existential variables) found by ProB
	**<tt>store</tt> to store the solution bindings as local variables (similar to let)		**<tt>store</tt> to store the solution bindings as local variables (similar to let)
	** <tt>ascii</tt> to print the result as ASCII rather than using Latex ~~mathssymbols~~		** <tt>ascii</tt> to print the result as ASCII rather than using Latex math symbols
	** <tt>time</tt> to display the time taken for the command		** <tt>time</tt> to display the time taken for the command
	** <tt>print</tt> to print the expression/predicate being evaluated (automatically set by <tt>\problet</tt>		** <tt>print</tt> to print the expression/predicate being evaluated (automatically set by <tt>\problet</tt>
Line 38:		Line 42:
	* <tt>\probdot{DOT}{File1}</tt> command takes a B expression <tt>EXPR</tt>as argument, evaluates it as a graph and writes a dot file <tt>File1</tt>. You can provide a second File as argument, in which case <tt>dot</tt> is called to generate a PDF document. You can also set <tt>sfdp</tt> as third argument, in which case the <tt>sfdp</tt> tool will be used instead of <tt>dot</tt>.		* <tt>\probdot{DOT}{File1}</tt> command takes a B expression <tt>EXPR</tt>as argument, evaluates it as a graph and writes a dot file <tt>File1</tt>. You can provide a second File as argument, in which case <tt>dot</tt> is called to generate a PDF document. You can also set <tt>sfdp</tt> as third argument, in which case the <tt>sfdp</tt> tool will be used instead of <tt>dot</tt>.

	* <tt>\probprint{EXRP}</tt> command takes a B expression or predicate <tt>EXPR</tt>as argument and pretty prints it.		* <tt>\probprint{EXRP}</tt> command takes a B expression or predicate <tt>EXPR</tt>as argument and pretty prints it. Optional arguments are:
			**<tt>pred</tt> only try to parse first argument as predicate
			**<tt>expr</tt> only try to parse first argument as expression
			**<tt>ascii</tt> to print the result as ASCII rather than using Latex math symbols

	* <tt>\probif{EXPR}{Then}{Else}</tt> command takes an expression or predicate <tt>EXPR</tt> and two Latex texts. If the expression evaluates to TRUE the first branch <tt>Then</tt> is processed, otherwise the other one <tt>Else</tt> is processed.		* <tt>\probif{EXPR}{Then}{Else}</tt> command takes an expression or predicate <tt>EXPR</tt> and two Latex texts. If the expression evaluates to TRUE the first branch <tt>Then</tt> is processed, otherwise the other one <tt>Else</tt> is processed.

	* <tt>\probfor{ID}{Set}{Body}</tt> command takes an identifier <tt>ID</tt>, a set expression <tt>Set</tt> and a Latex text <tt>Body</tt>, and processes the Latex text for every element of the set expression, setting the identifier to a value of the set.		* <tt>\probfor{ID}{Set}{Body}</tt> command takes an identifier <tt>ID</tt>, a set expression <tt>Set</tt> and a Latex text <tt>Body</tt>, and processes the Latex text for every element of the set expression, setting the identifier to a value of the set.

Michael Leuschel: /* Commands */

2016-09-07T11:32:06Z

Commands

← Older revision		Revision as of 11:32, 7 September 2016
Line 26:		Line 26:
	* <tt>\probexpr{EXRP}</tt> command takes a B expression <tt>EXPR</tt>as argument and evaluates it. By default it shows the B expression and the value of the expression. Example: <tt>\probexpr{{1}\/{2**10}}</tt> will be replaced by <tt>{1,1024}</tt>		* <tt>\probexpr{EXRP}</tt> command takes a B expression <tt>EXPR</tt>as argument and evaluates it. By default it shows the B expression and the value of the expression. Example: <tt>\probexpr{{1}\/{2**10}}</tt> will be replaced by <tt>{1,1024}</tt>

	* <tt>\probrepl{CMD}</tt> command takes a probcli REPL command <tt>CMD</tt> as argument and executes it. By default it shows only the output of the execution, e.g., in case it is a predicate TRUE or FALSE. Example: <tt>\probrepl{let DOM = 1..3}</tt>. A variation of the latter is the new command <tt>\problet{DOM}{1..3}</tt> which shows the let construct itself within the generated Latex.		* <tt>\probrepl{CMD}</tt> command takes a probcli REPL command <tt>CMD</tt> as argument and executes it. By default it shows only the output of the execution, e.g., in case it is a predicate TRUE or FALSE. Example: <tt>\probrepl{let DOM = 1..3}</tt>. A variation of the latter is the new command <tt>\problet{DOM}{1..3}</tt> which shows the let construct itself within the generated Latex. Optional arguments for <tt>\probrep<\tt> are :
			**<tt>solution</tt> to display the solution bindings (for existential variables) found by ProB
			**<tt>store</tt> to store the solution bindings as local variables (similar to let)
			** <tt>ascii</tt> to print the result as ASCII rather than using Latex mathssymbols
			** <tt>time</tt> to display the time taken for the command
			** <tt>print</tt> to print the expression/predicate being evaluated (automatically set by <tt>\problet</tt>
			** <tt>silent</tt> to not print the result of the evaluation

	* <tt>\probtable{EXRP}</tt> command takes a B expression <tt>EXPR</tt>as argument, evaluates it and shows it as a Latex table. Optional arguments are <tt>no-tabular</tt>, <tt>no-hline</tt>, <tt>no-headings</tt>, <tt>no-row-numbers</tt>, <tt>max-table-size=NR</tt>.		* <tt>\probtable{EXRP}</tt> command takes a B expression <tt>EXPR</tt>as argument, evaluates it and shows it as a Latex table. Optional arguments are <tt>no-tabular</tt>, <tt>no-hline</tt>, <tt>no-headings</tt>, <tt>no-row-numbers</tt>, <tt>max-table-size=NR</tt>.

	* <tt>\probdot{DOT}{File1}</tt> command takes a B expression <tt>EXPR</tt>as argument, evaluates it as a graph and writes a dot file <tt>File1</tt>. You can provide a second File as argument, in which case <tt>dot</tt> is called to generate a PDF document.		* <tt>\probdot{DOT}{File1}</tt> command takes a B expression <tt>EXPR</tt>as argument, evaluates it as a graph and writes a dot file <tt>File1</tt>. You can provide a second File as argument, in which case <tt>dot</tt> is called to generate a PDF document. You can also set <tt>sfdp</tt> as third argument, in which case the <tt>sfdp</tt> tool will be used instead of <tt>dot</tt>.

	* <tt>\probprint{EXRP}</tt> command takes a B expression or predicate <tt>EXPR</tt>as argument and pretty prints it.		* <tt>\probprint{EXRP}</tt> command takes a B expression or predicate <tt>EXPR</tt>as argument and pretty prints it.

Michael Leuschel: /* Commands */

2016-09-07T11:26:54Z

Commands

← Older revision		Revision as of 11:26, 7 September 2016
Line 26:		Line 26:
	* <tt>\probexpr{EXRP}</tt> command takes a B expression <tt>EXPR</tt>as argument and evaluates it. By default it shows the B expression and the value of the expression. Example: <tt>\probexpr{{1}\/{2**10}}</tt> will be replaced by <tt>{1,1024}</tt>		* <tt>\probexpr{EXRP}</tt> command takes a B expression <tt>EXPR</tt>as argument and evaluates it. By default it shows the B expression and the value of the expression. Example: <tt>\probexpr{{1}\/{2**10}}</tt> will be replaced by <tt>{1,1024}</tt>

	* <tt>\probrepl{CMD}</tt> command takes a probcli REPL command <tt>CMD</tt> as argument and executes it. By default it shows only the output of the execution, e.g., in case it is a predicate TRUE or FALSE. Example: <tt>\probrepl{let DOM = 1..3}</tt>.		* <tt>\probrepl{CMD}</tt> command takes a probcli REPL command <tt>CMD</tt> as argument and executes it. By default it shows only the output of the execution, e.g., in case it is a predicate TRUE or FALSE. Example: <tt>\probrepl{let DOM = 1..3}</tt>. A variation of the latter is the new command <tt>\problet{DOM}{1..3}</tt> which shows the let construct itself within the generated Latex.

	* <tt>\probtable{EXRP}</tt> command takes a B expression <tt>EXPR</tt>as argument, evaluates it and shows it as a Latex table.		* <tt>\probtable{EXRP}</tt> command takes a B expression <tt>EXPR</tt>as argument, evaluates it and shows it as a Latex table. Optional arguments are <tt>no-tabular</tt>, <tt>no-hline</tt>, <tt>no-headings</tt>, <tt>no-row-numbers</tt>, <tt>max-table-size=NR</tt>.

	* <tt>\probdot{DOT}{File1}</tt> command takes a B expression <tt>EXPR</tt>as argument, evaluates it as a graph and writes a dot file <tt>File1</tt>. You can provide a second File as argument, in which case <tt>dot</tt> is called to generate a PDF document.		* <tt>\probdot{DOT}{File1}</tt> command takes a B expression <tt>EXPR</tt>as argument, evaluates it as a graph and writes a dot file <tt>File1</tt>. You can provide a second File as argument, in which case <tt>dot</tt> is called to generate a PDF document.

Michael Leuschel: /* Commands */

2016-07-26T13:37:26Z

Commands

← Older revision		Revision as of 13:37, 26 July 2016
Line 26:		Line 26:
	* <tt>\probexpr{EXRP}</tt> command takes a B expression <tt>EXPR</tt>as argument and evaluates it. By default it shows the B expression and the value of the expression. Example: <tt>\probexpr{{1}\/{2**10}}</tt> will be replaced by <tt>{1,1024}</tt>		* <tt>\probexpr{EXRP}</tt> command takes a B expression <tt>EXPR</tt>as argument and evaluates it. By default it shows the B expression and the value of the expression. Example: <tt>\probexpr{{1}\/{2**10}}</tt> will be replaced by <tt>{1,1024}</tt>

	* <tt>\probrepl{CMD}</tt> command takes a probcli REPL command <tt>CMD</tt>as argument and executes it. By default it shows only the output of the execution, e.g., in case it is a predicate TRUE or FALSE. Example: <tt>\probrepl{let DOM = 1..3}</tt>.		* <tt>\probrepl{CMD}</tt> command takes a probcli REPL command <tt>CMD</tt> as argument and executes it. By default it shows only the output of the execution, e.g., in case it is a predicate TRUE or FALSE. Example: <tt>\probrepl{let DOM = 1..3}</tt>.

	* <tt>\probtable{EXRP}</tt> command takes a B expression <tt>EXPR</tt>as argument, evaluates it and shows it as a Latex table.		* <tt>\probtable{EXRP}</tt> command takes a B expression <tt>EXPR</tt>as argument, evaluates it and shows it as a Latex table.

Michael Leuschel: /* Commands */

2016-07-26T13:37:07Z

Commands

← Older revision		Revision as of 13:37, 26 July 2016
Line 24:		Line 24:
	The commands are described in the PDF document above.		The commands are described in the PDF document above.
	Here is a short summary of some of the commands:		Here is a short summary of some of the commands:
	* <tt>\probexpr{EXRP}</tt> command takes a B expression <tt>EXPR</tt>as argument and evaluates it.		* <tt>\probexpr{EXRP}</tt> command takes a B expression <tt>EXPR</tt>as argument and evaluates it. By default it shows the B expression and the value of the expression. Example: <tt>\probexpr{{1}\/{2**10}}</tt> will be replaced by <tt>{1,1024}</tt>
	By default it shows the B expression and the value of the expression. Example: <tt>\probexpr{{1}\/{2**10}}</tt> will be replaced by <tt>{1,1024}</tt>
	* <tt>\probrepl{CMD}</tt> command takes a probcli REPL command <tt>CMD</tt>as argument and executes it. By default it shows only the output of the execution, e.g., in case it is a predicate TRUE or FALSE. Example: <tt>\probrepl{let DOM = 1..3}</tt>.		* <tt>\probrepl{CMD}</tt> command takes a probcli REPL command <tt>CMD</tt>as argument and executes it. By default it shows only the output of the execution, e.g., in case it is a predicate TRUE or FALSE. Example: <tt>\probrepl{let DOM = 1..3}</tt>.

	* <tt>\probtable{EXRP}</tt> command takes a B expression <tt>EXPR</tt>as argument, evaluates it and shows it as a Latex table.		* <tt>\probtable{EXRP}</tt> command takes a B expression <tt>EXPR</tt>as argument, evaluates it and shows it as a Latex table.

	* <tt>\probdot{DOT}{File1}</tt> command takes a B expression <tt>EXPR</tt>as argument, evaluates it as a graph and writes a dot file <tt>File1</tt>. You can provide a second File as argument, in which case <tt>dot</tt> is called to generate a PDF document.		* <tt>\probdot{DOT}{File1}</tt> command takes a B expression <tt>EXPR</tt>as argument, evaluates it as a graph and writes a dot file <tt>File1</tt>. You can provide a second File as argument, in which case <tt>dot</tt> is called to generate a PDF document.

	* <tt>\probprint{EXRP}</tt> command takes a B expression or predicate <tt>EXPR</tt>as argument and pretty prints it.		* <tt>\probprint{EXRP}</tt> command takes a B expression or predicate <tt>EXPR</tt>as argument and pretty prints it.

	* <tt>\probif{EXPR}{Then}{Else}</tt> command takes an expression or predicate <tt>EXPR</tt> and two Latex texts. If the expression evaluates to TRUE the first branch <tt>Then</tt> is processed, otherwise the other one <tt>Else</tt> is processed.		* <tt>\probif{EXPR}{Then}{Else}</tt> command takes an expression or predicate <tt>EXPR</tt> and two Latex texts. If the expression evaluates to TRUE the first branch <tt>Then</tt> is processed, otherwise the other one <tt>Else</tt> is processed.

	* <tt>\probfor{ID}{Set}{Body}</tt> command takes an identifier <tt>ID</tt>, a set expression <tt>Set</tt> and a Latex text <tt>Body</tt>, and processes the Latex text for every element of the set expression, setting the identifier to a value of the set.		* <tt>\probfor{ID}{Set}{Body}</tt> command takes an identifier <tt>ID</tt>, a set expression <tt>Set</tt> and a Latex text <tt>Body</tt>, and processes the Latex text for every element of the set expression, setting the identifier to a value of the set.