kfhoech
commented
4 years ago 
Jen -
I would be very interested in the structure of these models. I wonder if there is something we can do to speed 'em up. Also, if AGREE saved off advice (the jkind -advice directive), it is very likely that this would substantially speed up your analysis. If the models were unchanged, analysis should only require a few seconds.
Mike
On Mon, May 7, 2018 at 4:04 PM, Jennifer Davis notifications@github.com wrote:
My recent work has involved analysis runs that take a day or more to complete. A feature that auto-saved results would help save me time of taking screenshots and opening and saving counterexamples. It would help prevent user error and would be very beneficial in the event that some sort of system interrupt (forced computer restart, etc.) happens after analysis completes but before I save off the results. Ideally, such a feature would do the following:
- Emit results to a predictable, intuitive location. I suggest my_AADL_project_folder/results or perhaps my_AADL_project_folder/aadl/ results
- Emit a summary table of results and any counterexamples found by the model checker to separate files. The summary table should include the information shown in the AGREE Results tab (name of property, result, and analysis time). The form of the summary table could be *.csv or Excel. The counterexamples could simply be the Excel files emitted when the user opens the counterexample from the GUI.
- Emit a short text file with the user's analysis settings for the run.
- Append a timestamp from when the run was started to the auto-generated filenames. This should prevent accidentally overwriting previous results.
Auto-saving results could be an optional feature that the user selects from the Preferences menu.
— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/smaccm/smaccm/issues/134, or mute the thread https://github.com/notifications/unsubscribe-auth/AE-aulWrhXBCgvt6RZU8W1vEh-T-du3dks5twLbTgaJpZM4T1o_R .
-- Michael Whalen Director, University of Minnesota Software Engineering Center (UMSEC) 200 Union St. 4-192 Minneapolis, MN 55455 Office: 612-624-5130 Cell: 651-442-8834
My recent work has involved analysis runs that take a day or more to complete. A feature that auto-saved results would help save me time of taking screenshots and opening and saving counterexamples. It would help prevent user error and would be very beneficial in the event that some sort of system interrupt (forced computer restart, etc.) happens after analysis completes but before I save off the results. Ideally, such a feature would do the following:
1) Emit results to a predictable, intuitive location. I suggest my_AADL_project_folder/results or my_AADL_project_folder/aadl/results or maybe folder_containing_AADL_file_being_run/[AADL_filename]_results 2) Emit a summary table of results, the agree_advice file, and any counterexamples found by the model checker to separate files. The summary table should include the information shown in the AGREE Results tab (name of property, result, and analysis time). The form of the summary table could be *.csv or Excel. The counterexamples could simply be the Excel files emitted when the user opens the counterexample from the GUI. 3) Emit a short text file with the user's analysis settings for the run. 4) Append a timestamp from when the run was started to the auto-generated filenames. This should prevent accidentally overwriting previous results.
Auto-saving results could be an optional feature that the user selects from the Preferences menu.