ada/OpenUxAS
0
0
Fork 0
mirror of https://github.com/AdaCore/OpenUxAS.git synced 2026-02-12 13:07:16 -08:00
Code Issues Packages Projects Releases Wiki Activity

Commit Graph

  • 375c977ee0 Improve run_example.py develop M. Anthony Aiello 2022-03-15 17:15:26 -04:00
  • 57c299e89e Improve support from running LmcpGen; refactor. M. Anthony Aiello 2022-03-11 15:40:21 -05:00
  • fbc0e3eed9 Update proofs for Route Aggregator and Assignment Tree Branch and Bound (#41) lhumphrey 2021-11-05 11:40:37 -04:00
  • c087aac77b Merge pull request #37 from joffreyhuguet/silver_level_proof_algebra_tree M. Anthony Aiello 2021-10-28 15:14:41 -04:00
  • 7bbdaa3c3e Update session files and proof testsuite Joffrey Huguet 2021-10-22 13:48:28 +02:00
  • 37be0e7333 Merge pull request #36 from AdaCore/integration Joffrey Huguet 2021-10-25 16:58:58 +02:00
  • 7fcf0280fc Silver-level proof of algebra tree generation Joffrey Huguet 2021-10-19 16:28:01 +02:00
  • 77da5a56aa Update the install scripts for CE21 (#35) M. Anthony Aiello 2021-10-21 11:23:48 -04:00
  • f8859bde87 Merge pull request #29 from joffreyhuguet/improve_proof_testsuite Joffrey Huguet 2021-10-21 17:13:52 +02:00
  • bf2ca34d75 Complete silver-level proof of main functionality of Assignment Tree Branch Bound Joffrey Huguet 2021-03-31 11:27:48 +02:00
  • 61b336ab7c Update session files and testsuite Joffrey Huguet 2021-10-21 15:21:02 +02:00
  • a04e130b3b Complete silver-level proof of main functionality of Assignment Tree Branch Bound Joffrey Huguet 2021-03-31 11:27:48 +02:00
  • 5f28a40c35 Implement new assumption in ARV In order to prove the ATBB, an assumption has to be made about the ARV service; it should always output a non-empty list of eligible entities for an AutomationRequest. If the received AutomationRequest has a non-empty EntityList, nothing is changed. In the other case, it is replaced by the list of entities whose ARV service has Configuration and State available at the moment it processes the AutomationRequest. Joffrey Huguet 2021-08-19 11:06:43 +02:00
  • 99054911e4 Merge branch 'integration' into improve_proof_testsuite Joffrey Huguet 2021-10-20 10:15:00 +02:00
  • f8ee438e26 Merge pull request #34 from joffreyhuguet/update_to_community2021 Joffrey Huguet 2021-10-19 17:16:04 +02:00
  • 0192696235 Merge pull request #32 from pat-rogers/integration Pat Rogers 2021-10-19 09:34:45 -05:00
  • e88b1d0678 fix problem with static call to non-abstract subprogram... highlighted by Community Edition 2021 rogers 2021-10-18 16:41:43 -05:00
  • 16adbf1d57 Merge branch 'integration' into DAIDALUS_integration DAIDALUS_integration M. Anthony Aiello 2021-09-27 15:53:43 -04:00
  • ea0e4a2fd9 Improve run-proofs.py to allow to run on non-replay mode, to easily rewrite session files Joffrey Huguet 2021-08-23 09:30:06 +02:00
  • f9dc0ab69e Add a proof-of-concept model of the RA. experiments/lustre M. Anthony Aiello 2021-09-02 17:25:23 -04:00
  • a0f5fe3df3 Minor cleanup. M. Anthony Aiello 2021-09-02 17:24:54 -04:00
  • 9bbf1e6c16 Merge pull request #35 from AdaCore/integration lhumphrey 2021-08-25 15:57:24 -04:00
  • 321f0bfcd8 Fix errors for RunLmcpGen.py (#30) M. Anthony Aiello 2021-08-25 15:16:51 -04:00
  • 75b2dff91d Adjust variables in Ada code to run the demos properly Joffrey Huguet 2021-08-19 11:15:09 +02:00
  • ad985645b6 Update daidalus_integration with new infrastructure (#28) M. Anthony Aiello 2021-08-17 09:48:38 -04:00
  • ee500fc6b8 Use GNAT Community Edition 2021 in GitHub Actions Joffrey Huguet 2021-07-28 09:32:48 +02:00
  • 57319a5a39 Update session files for CE2021 Joffrey Huguet 2021-07-26 17:26:20 +02:00
  • 806867534f Update files to prove with CE2021 Joffrey Huguet 2021-07-26 16:53:41 +02:00
  • e80b61bb7f Remove asserts and improve bus. M. Anthony Aiello 2021-07-21 16:37:19 -04:00
  • 3396482499 Refactoring and working contract-based proofs. M. Anthony Aiello 2021-07-21 14:02:37 -04:00
  • f5dcc92fdd Refactor uxas M. Anthony Aiello 2021-07-14 16:42:35 -04:00
  • 969aa0a4da Improved properties for Task. M. Anthony Aiello 2021-07-08 12:09:45 -04:00
  • 2eb96796c2 Update the abstract Task with stronger P2. M. Anthony Aiello 2021-07-08 09:56:38 -04:00
  • c62c4b2518 WIP on enhancement. M. Anthony Aiello 2021-07-07 17:13:09 -04:00
  • 1df751b817 Merge pull request #32 from AdaCore/integration lhumphrey 2021-07-07 13:32:18 -04:00
  • a52e58750b Merge pull request #31 from AdaCore/bugfix/tox-configuration lhumphrey 2021-07-07 12:53:37 -04:00
  • 6ac7f1ed5c Merge pull request #25 from joffreyhuguet/implement_greedy_exploration_atbb Joffrey Huguet 2021-07-07 16:58:59 +02:00
  • 010a625627 Update uxas tox for mypy and bandit (#27) M. Anthony Aiello 2021-07-07 10:29:11 -04:00
  • 5a81a3aefe Implement greedy traversal of the "search tree" in the Ada Assignment Tree Branch Bound It is unnecessary to compute the greedy solution since it will be the first explored leaf of the tree Joffrey Huguet 2021-03-30 14:27:19 +02:00
  • 28dea43272 Update uxas-module.yaml lhumphrey 2021-07-06 09:51:18 -04:00
  • f605997e6a Update uxas-module.yaml lhumphrey 2021-07-06 09:48:28 -04:00
  • 0cd925d54a Update uxas-module.yaml lhumphrey 2021-07-06 09:45:34 -04:00
  • 54ebe50f26 Update uxas-module.yaml lhumphrey 2021-07-06 09:36:44 -04:00
  • dfd0c9e3dc Completed prototype partial TLA+ model for ARV. experiments/tla M. Anthony Aiello 2021-07-01 10:02:01 -04:00
  • a6894a8314 Further refactoring to improve the model. M. Anthony Aiello 2021-06-10 15:55:09 -04:00
  • 9dd92b66cd Enhance the model. M. Anthony Aiello 2021-06-10 11:39:39 -04:00
  • 2102b55476 Complete OpenUxAS model in lustre. M. Anthony Aiello 2021-06-07 11:07:15 -04:00
  • abdd846415 Final Properties for UxAS model. M. Anthony Aiello 2021-06-04 18:38:02 -04:00
  • 1a10d6393f Reorganize and clean up model. M. Anthony Aiello 2021-06-04 12:01:36 -04:00
  • be41106e5c Complete model updates with stronger properties. M. Anthony Aiello 2021-06-04 11:22:55 -04:00
  • 887576b453 Update uxas-module.yaml lhumphrey 2021-05-27 10:23:35 -04:00
  • 37de997bb5 Update uxas-cpp.yml lhumphrey 2021-05-27 10:21:28 -04:00
  • da60a2ff27 Update uxas-ada.yml lhumphrey 2021-05-27 10:19:26 -04:00
  • fdf6c618a6 Update infrastructure-install.yaml lhumphrey 2021-05-27 10:17:00 -04:00
  • 8b82c5c6e0 Update amase.yml lhumphrey 2021-05-27 10:04:05 -04:00
  • 0954458ea3 Merge pull request #29 from lhumphrey/develop lhumphrey 2021-05-26 17:14:37 -04:00
  • 5b9386a0ff Updated location of boost download lhumphrey 2021-05-26 17:13:33 -04:00
  • 1710079a26 Merge pull request #28 from lhumphrey/develop lhumphrey 2021-05-26 16:57:44 -04:00
  • 2d85cfa206 Updated location of boost download lhumphrey 2021-05-26 16:55:48 -04:00
  • 59b3b064b7 Partial rework of WM M. Anthony Aiello 2021-05-26 16:41:15 -04:00
  • 2f96168e03 Update ARV to use a much better requirement M. Anthony Aiello 2021-05-26 16:39:10 -04:00
  • 06872a5089 Merge pull request #27 from lhumphrey/develop lhumphrey 2021-05-26 16:16:13 -04:00
  • e1078e1122 Update uxas-cpp.yml lhumphrey 2021-05-26 14:24:34 -04:00
  • 8df6c42673 Update uxas-module.yaml lhumphrey 2021-05-26 14:15:59 -04:00
  • bebe2b27ed Updated location of boost download lhumphrey 2021-05-26 14:06:26 -04:00
  • 465e1e4369 Merge pull request #26 from BenHocking/develop lhumphrey 2021-05-26 13:28:10 -04:00
  • c42fc5ccd3 Progress towards compositional proof. M. Anthony Aiello 2021-05-26 11:20:41 -04:00
  • df5ebc4769 Enhancements to the model. M. Anthony Aiello 2021-05-24 17:24:33 -04:00
  • 2605cde73d Fixes errCalculateCentroid to use East instead of North when summing the total contributions from the East. BenHocking 2021-05-18 15:41:37 -04:00
  • c3ab1893d1 Updates to the OpenUxAS model. M. Anthony Aiello 2021-04-26 13:46:23 -04:00
  • f8605e61ca Merge pull request #25 from lhumphrey/develop lhumphrey 2021-04-12 14:45:44 -04:00
  • 4293b4c70e Updated amase2uxas.py for python3 lhumphrey 2021-04-12 14:44:26 -04:00
  • f0a222fa69 Add a poc for compositional reasoning M. Anthony Aiello 2021-04-02 17:14:31 -04:00
  • 53a4d45255 Merge pull request #23 from AdaCore/integration lhumphrey 2021-04-02 11:49:19 -04:00
  • f4f5b3cb4b Merge pull request #24 from lhumphrey/develop lhumphrey 2021-04-01 16:30:40 -04:00
  • 289d28022b example template lhumphrey 2021-04-01 15:38:23 -04:00
  • 5712513b30 Bootstrap Integration (#24) M. Anthony Aiello 2021-04-01 15:30:51 -04:00
  • 0c6cf4aec2 Improved WM and ARV and initial compositional prop M. Anthony Aiello 2021-03-12 17:23:30 -05:00
  • 649349d7d6 Compositional proof over WM and ARV using new mdl. M. Anthony Aiello 2021-03-11 17:42:54 -05:00
  • 162f709f55 Refactor to break uxas3 into modular pieces. M. Anthony Aiello 2021-03-10 14:44:32 -05:00
  • 3377143d1e Add a new uxas and a working theory of sequences. M. Anthony Aiello 2021-03-10 14:15:05 -05:00
  • 45d8327549 Add an updated model for OpenUxAS M. Anthony Aiello 2021-03-04 14:26:03 -05:00
  • d0a00fb003 Remove workflows. M. Anthony Aiello 2021-03-04 11:17:40 -05:00
  • 4a4400a7fb Add Proofs of Concept with README M. Anthony Aiello 2021-03-04 11:14:04 -05:00
  • 5215043825 Initial lustre model for OpenUxAS with README. M. Anthony Aiello 2021-03-04 11:10:27 -05:00
  • 20e198e918 Documentation for adding new examples to run-example (#20) M. Anthony Aiello 2021-01-26 15:34:41 -05:00
  • c5a83d2bf9 Merge pull request #21 from AdaCore/feature/change-proof-report-level lhumphrey 2021-01-26 15:33:48 -05:00
  • be3b58d961 Merge pull request #21 from joffreyhuguet/change_reporting_level_in_proof_testsuite Joffrey Huguet 2021-01-25 16:59:36 +01:00
  • ea8435be52 Merge pull request #19 from AdaCore/integration lhumphrey 2021-01-20 15:32:54 -05:00
  • d69697f5d9 Merge pull request #19 from joffreyhuguet/atbb_silver_level_proof Joffrey Huguet 2020-12-08 14:13:36 +01:00
  • 13ef200985 Partial silver-level proof of ATBB service functionality Three assertions remain unproved Joffrey Huguet 2020-12-07 11:10:38 +01:00
  • e56a071400 Merge pull request #18 from joffreyhuguet/spark_code_cleanup Joffrey Huguet 2020-12-07 11:43:23 +01:00
  • 88a40f522c Update session files and testsuite Joffrey Huguet 2020-12-04 11:45:13 +01:00
  • 8ad72e3f25 Cleanup of SPARK files Joffrey Huguet 2020-12-03 15:40:24 +01:00
  • 5eeacade1a fix style casing errors to match generated/copied files from lmcpgen, for TB04-026 rogers 2020-11-20 16:05:35 -06:00
  • 2914163b00 Merge pull request #17 from joffreyhuguet/fix_actions Joffrey Huguet 2020-12-04 16:40:52 +01:00
  • 642ec64775 Reference ada-actions/toolchain@ce2020 in Actions script instead of v0.2.0 Joffrey Huguet 2020-11-24 17:43:09 +01:00
  • c1cc64ad5c fix style casing errors to match generated/copied files from lmcpgen, for TB04-026 rogers/casing_fix rogers 2020-11-20 16:05:35 -06:00
  • f22e51cf1e Merge pull request #15 from joffreyhuguet/update_arv_service Joffrey Huguet 2020-10-29 09:11:26 +01:00
  • 59358ed71a Update session files and testsuite Joffrey Huguet 2020-10-23 09:35:35 +02:00