Figure : Failed Property When a property fails in AGREE, there is an associated counterexample that demonstrates the failure. To see the counterexample, right-click the failing property (in this case: output range”) and “System choose Counterexample in Console” to see the values assigned to each of the variables “View referenced in the model. Figure 7 shows the counterexample that is generated by this failure in the console window. Figure : Counterexample For working with complex counterexamples, it is often necessary to have a richer interface. It is also possible to export the counterexample to Excel by right-clicking the failing property and choosing “View Counterexample in Excel”. NB: In order to use this capability, you must have Excel installed on your computer. Also, you must associate .xls files in Eclipse with Excel. To do so, choose the menu item from the Window menu, then “Preferences” On the left side of the dialog box, choose General > Editors > File Associations, then the button next to Types” and then “Add…” “File type into the text box. “*.xls” The .xls file type should now be selected. Now choose the button next to Editors” “Add…” “Associated Choose the Programs” radio button “External Select Excel Worksheet” and click OK. “Microsoft The generated Excel file for the example is shown in Figure 8. Figure : Excel Counterexample File Note that this counterexample is only one step long. If it were multiple these would be displayed in consecutive columns from left to right. When executed with real-valued inputs and outputs, it is possible to find a counterexample to the system-level property. In this counterexample, the system input is 9.5, so it is less than 10, but the system output is equal to 50, violating the system guarantee. Can you find the reason for the counterexample?
Figure : Failed Property When a property fails in AGREE, there is an associated counterexample that demonstrates the failure. To see the counterexample, right-click the failing property (in this case: “System output range”) and choose “View Counterexample in Console” to see the values assigned to each of the variables referenced in the model. Figure 7 shows the counterexample that is generated by this failure in the console window. Figure : Counterexample For working with complex counterexamples, it is often necessary to have a richer interface. It is also possible to export the counterexample to Excel by right-clicking the failing property and choosing “View Counterexample in Excel”. NB: In order to use this capability, you must have Excel installed on your computer. Also, you must associate .xls files in Eclipse with Excel. To do so, choose the “Preferences” menu item from the Window menu, then On the left side of the dialog box, choose General > Editors > File Associations, then the “Add…” button next to “File Types” and then type “*.xls” into the text box. The .xls file type should now be selected. Now choose the “Add…” button next to “Associated Editors” Choose the “External Programs” radio button Select “Microsoft Excel Worksheet” and click OK. The generated Excel file for the example is shown in Figure 8. Figure : Excel Counterexample File Note that this counterexample is only one step long. If it were multiple these would be displayed in consecutive columns from left to right. When executed with real-valued inputs and outputs, it is possible to find a counterexample to the system-level property. In this counterexample, the system input is 9.5, so it is less than 10, but the system output is equal to 50, violating the system guarantee. Can you find the reason for the counterexample?
AGREE%20Users%20Guide.docx