Evaluation View - Revision history

Michael Leuschel: /* Understanding the Invariant and Properties */

2011-11-20T15:47:19Z

Understanding the Invariant and Properties

← Older revision		Revision as of 15:47, 20 November 2011
Line 65:		Line 65:
	END		END

	we can now model check the machine and ~~will~~ find a counter ~~exaple~~ that can be inspected using the evaluation view and because of the automatically introduced predicate it is very easy to see the reason why <tt>magazines <: papers</tt> is false.		we can now model check the machine and find a counter example that can be inspected using the evaluation view and because of the automatically introduced predicate it is very easy to see the reason why <tt>magazines <: papers</tt> is false.

	[[File:Eval_view6.png\|500px]]		[[File:Eval_view6.png\|500px]]

Jens Bendisposto: /* Filtering relevant information and Data Extraction */

2011-10-07T12:07:06Z

Filtering relevant information and Data Extraction

← Older revision		Revision as of 12:07, 7 October 2011
Line 76:		Line 76:
	[[File:Eval_view7.png\|500px]]		[[File:Eval_view7.png\|500px]]

	The second way to filter out unnecessary ~~noise~~ is to mark some items and restrict the view. Suppose we are only interested in the constants x1, x4, x17 and the property <tt>(x4 = FALSE or X2=FALSE) or X6=TRUE</tt> (the first property in the list). Using the right mouse button, we can mark all the rows in the view that we want to see by selecting Mark from the ~~popup~~ menu. In the same popup menu, we can select "Show only marked items" which will remove all other information.		The second way to filter out unnecessary information is to mark some items and restrict the view. Suppose we are only interested in the constants x1, x4, x17 and the property <tt>(x4 = FALSE or X2=FALSE) or X6=TRUE</tt> (the first property in the list). Using the right mouse button, we can mark all the rows in the view that we want to see by selecting "Mark all selected items" from the context menu. In the same popup menu, we can select "Show only marked items" which will remove all other information.

	[[File:Eval_view8.png\|500px]]		[[File:Eval_view8.png\|500px]]

Jens Bendisposto: /* Filtering relevant information */

2011-10-07T11:53:59Z

Filtering relevant information

← Older revision		Revision as of 11:53, 7 October 2011
Line 69:		Line 69:
	[[File:Eval_view6.png\|500px]]		[[File:Eval_view6.png\|500px]]

	== Filtering relevant information ==		== Filtering relevant information and Data Extraction ==
	There are two different ways to filter out important information from a state. To demonstrate this feature we can use the model SATLIB_blocksworld_medium.mch from the LessSimple folder of the ProB distribution. After executing SETUP_CONSTANTS and INITIALISATION we open the evaluation view. It contains a large number of constants and properties that might not be equally interesting.		There are two different ways to filter out important information from a state. To demonstrate this feature we can use the model SATLIB_blocksworld_medium.mch from the LessSimple folder of the ProB distribution. After executing SETUP_CONSTANTS and INITIALISATION we open the evaluation view. It contains a large number of constants and properties that might not be equally interesting.

Line 79:		Line 79:

	[[File:Eval_view8.png\|500px]]		[[File:Eval_view8.png\|500px]]

			Finally the popup menu allows us to save the content of a particular state into a file (either the full state, or the marked items only). In either case, ProB will generate a text file containing the state as a predicate. In our example the file will contain the following predicate

			x1 = FALSE
			&
			x4 = TRUE
			&
			x17 = TRUE
			&
			(x4 = FALSE or x2 = FALSE) or x6 = TRUE

Jens Bendisposto: /* Data Extraction */

2011-10-07T11:50:28Z

Data Extraction

← Older revision		Revision as of 11:50, 7 October 2011
Line 79:		Line 79:

	[[File:Eval_view8.png\|500px]]		[[File:Eval_view8.png\|500px]]

	~~== Data Extraction ==~~

Jens Bendisposto: /* Filtering relevant information */

2011-10-07T11:40:11Z

Filtering relevant information

← Older revision		Revision as of 11:40, 7 October 2011
Line 70:		Line 70:

	== Filtering relevant information ==		== Filtering relevant information ==
	There are two different ways to filter out important information from a state. To demonstrate this feature we can use the model SATLIB_blocksworld_medium.mch from the LessSimple folder of the ProB distribution. After executing SETUP_CONSTANTS we open the evaluation view. It contains a large number of constants and properties that might not be equally interesting.		There are two different ways to filter out important information from a state. To demonstrate this feature we can use the model SATLIB_blocksworld_medium.mch from the LessSimple folder of the ProB distribution. After executing SETUP_CONSTANTS and INITIALISATION we open the evaluation view. It contains a large number of constants and properties that might not be equally interesting.

	The first way to filter out information is using the Search Box in the upper right part of the view. As we type, ProB will filter out all items that do not contain our search phrase. If we, for instance, type x19. We will get only those constants and properties that contain x19.		The first way to filter out information is using the Search Box in the upper right part of the view. As we type, ProB will filter out all items that do not contain our search phrase. If we, for instance, type x19. We will get only those constants and properties that contain x19.

Jens Bendisposto: /* Filtering relevant information */

2011-10-07T11:38:31Z

Filtering relevant information

← Older revision		Revision as of 11:38, 7 October 2011
Line 76:		Line 76:
	[[File:Eval_view7.png\|500px]]		[[File:Eval_view7.png\|500px]]

	Suppose we are only interested in the constants x1, x4 ~~and~~ x17 and the property <tt>(x4 = FALSE or X2=FALSE) or X6=TRUE</tt> (the first property in the list).		The second way to filter out unnecessary noise is to mark some items and restrict the view. Suppose we are only interested in the constants x1, x4, x17 and the property <tt>(x4 = FALSE or X2=FALSE) or X6=TRUE</tt> (the first property in the list). Using the right mouse button, we can mark all the rows in the view that we want to see by selecting Mark from the popup menu. In the same popup menu, we can select "Show only marked items" which will remove all other information.

	Using the right mouse button, we can mark all the rows in the view that we want to see. ~~Also in~~ the popup menu, we can select "Show only marked items" which will remove all other information.

	[[File:Eval_view8.png\|500px]]		[[File:Eval_view8.png\|500px]]

	== Data Extraction ==		== Data Extraction ==

Jens Bendisposto: /* Filtering relevant information */

2011-10-07T11:36:37Z

Filtering relevant information

← Older revision		Revision as of 11:36, 7 October 2011
Line 72:		Line 72:
	There are two different ways to filter out important information from a state. To demonstrate this feature we can use the model SATLIB_blocksworld_medium.mch from the LessSimple folder of the ProB distribution. After executing SETUP_CONSTANTS we open the evaluation view. It contains a large number of constants and properties that might not be equally interesting.		There are two different ways to filter out important information from a state. To demonstrate this feature we can use the model SATLIB_blocksworld_medium.mch from the LessSimple folder of the ProB distribution. After executing SETUP_CONSTANTS we open the evaluation view. It contains a large number of constants and properties that might not be equally interesting.

	The first way to filter out information is using the Search Box in the upper right part of the view. as we type, ProB will filter ~~the~~ items ~~to only show those~~ that contain our search phrase. If we , for instance, type x19. We will get ~~all Constants~~ and properties that contain x19.		The first way to filter out information is using the Search Box in the upper right part of the view. As we type, ProB will filter out all items that do not contain our search phrase. If we, for instance, type x19. We will get only those constants and properties that contain x19.

	[[File:Eval_view7.png\|500px]]		[[File:Eval_view7.png\|500px]]

Jens Bendisposto: /* Filtering relevant information */

2011-10-07T11:35:32Z

Filtering relevant information

← Older revision		Revision as of 11:35, 7 October 2011
Line 72:		Line 72:
	There are two different ways to filter out important information from a state. To demonstrate this feature we can use the model SATLIB_blocksworld_medium.mch from the LessSimple folder of the ProB distribution. After executing SETUP_CONSTANTS we open the evaluation view. It contains a large number of constants and properties that might not be equally interesting.		There are two different ways to filter out important information from a state. To demonstrate this feature we can use the model SATLIB_blocksworld_medium.mch from the LessSimple folder of the ProB distribution. After executing SETUP_CONSTANTS we open the evaluation view. It contains a large number of constants and properties that might not be equally interesting.

	The first way to filter out information is using the Search Box on the upper right of the view. as we type, ProB will filter the items to only show those that contain our search phrase. If we , for instance, type x19. We will get all Constants and properties that contain x19.		The first way to filter out information is using the Search Box in the upper right part of the view. as we type, ProB will filter the items to only show those that contain our search phrase. If we , for instance, type x19. We will get all Constants and properties that contain x19.

	[[File:Eval_view7.png\|500px]]		[[File:Eval_view7.png\|500px]]

Jens Bendisposto: /* Filtering relevant information */

2011-10-07T11:35:06Z

Filtering relevant information

← Older revision		Revision as of 11:35, 7 October 2011
Line 70:		Line 70:

	== Filtering relevant information ==		== Filtering relevant information ==
	There are two different ways to filter out important information from a state. To demonstrate this feature we can use the model SATLIB_blocksworld_medium.mch from the LessSimple folder of the ProB distribution. After executing SETUP_CONSTANTS we open the evaluation view.		There are two different ways to filter out important information from a state. To demonstrate this feature we can use the model SATLIB_blocksworld_medium.mch from the LessSimple folder of the ProB distribution. After executing SETUP_CONSTANTS we open the evaluation view. It contains a large number of constants and properties that might not be equally interesting.

	The first way to filter out information is using the Search Box on the upper right of the view. as we type, ProB will filter the items to only show those that contain our search phrase. If we , for instance, type x19. We will get all Constants and properties that contain x19.		The first way to filter out information is using the Search Box on the upper right of the view. as we type, ProB will filter the items to only show those that contain our search phrase. If we , for instance, type x19. We will get all Constants and properties that contain x19.
Line 76:		Line 76:
	[[File:Eval_view7.png\|500px]]		[[File:Eval_view7.png\|500px]]

	~~It contains a large number of constants and properties.~~ Suppose we are only interested in the constants x1, x4 and x17 and the property <tt>(x4 = FALSE or X2=FALSE) or X6=TRUE</tt> (the first property in the list).		Suppose we are only interested in the constants x1, x4 and x17 and the property <tt>(x4 = FALSE or X2=FALSE) or X6=TRUE</tt> (the first property in the list).

	Using the right mouse button, we can mark all the rows in the view that we want to see. Also in the popup menu, we can select "Show only marked items" which will remove all other information.		Using the right mouse button, we can mark all the rows in the view that we want to see. Also in the popup menu, we can select "Show only marked items" which will remove all other information.

Jens Bendisposto: /* Filtering relevant information */

2011-10-07T11:33:30Z

Filtering relevant information

← Older revision		Revision as of 11:33, 7 October 2011
Line 76:		Line 76:
	[[File:Eval_view7.png\|500px]]		[[File:Eval_view7.png\|500px]]

	It contains a large number of constants and properties. Suppose we are only interested in the constants x1, x4 and x17 and the property <tt>(x4 = FALSE or X2=FALSE) or X6=TRUE</tt> (the first property in the list).		It contains a large number of constants and properties. Suppose we are only interested in the constants x1, x4 and x17 and the property <tt>(x4 = FALSE or X2=FALSE) or X6=TRUE</tt> (the first property in the list).

	Using the right mouse button, we can mark all the rows in the view that we want to see. Also in the popup menu, we can select "Show only marked items" which will remove all other information.		Using the right mouse button, we can mark all the rows in the view that we want to see. Also in the popup menu, we can select "Show only marked items" which will remove all other information.