974 Commits

Author SHA1 Message Date
M. Anthony Aiello
375c977ee0 Improve run_example.py
Recent updates to linters revealed a number of potential code-quality
issues.

Most were related to the use of f-strings in loggers, which is
discouraged because the string interpolation is greedy (happens even if
that logging level is disabled) and because it makes the job of log
aggregators more difficult (unlikely to matter to us).

There was an instance of use of a "global" that was not intended to be
such. This was spotted by moving the core script-like functionality into
a function, which avoided adding names to the global namespace.

The script is also renamed to conform to python module-naming
conventions.

All warnings and errors are resolved, except the overly broad catching
of Exception, which is explicitly silenced.

Add a workflow for running the HelloWorld example in CI as a simple
sanity check on run-example functionality.
2022-03-24 11:23:03 -04:00
M. Anthony Aiello
57c299e89e Improve support from running LmcpGen; refactor.
RunLmcpGen.py is renamed to run_lmcpgen.py, to be consistent with python
module naming guidelines.

run_lmcpgen.py is now wrapped by a shell script, `run-lmcpgen`. This
allows it to be used without requiring the user to manually activate the
python venv - just like run-example or anod. This also means that the
user is prompted to install infrastructure it needed.

Logging in run_lmcpgen.py is much improved: it is more verbose on info
(communicates what is being done to the user) and more accurate on
warning and critical (actually explain the problem correctly) and
provide remedial action (run anod devel-setup).

Logger config for run_lmcpgen.py and run-example.py is regularized
and refactored into uxas.util.logging - this eliminates redundant code
between the two files. e3 is still not required, but is used if
available.

A workflow has been added to GitHub Actions to test the invocation of
run-lmcpgen automatically.
2022-03-15 09:46:40 -04:00
lhumphrey
fbc0e3eed9 Update proofs for Route Aggregator and Assignment Tree Branch and Bound (#41)
* Added missing test.out file for route_aggregator

* Updated proof session files for Route Aggregator and Assignment Tree Branch and Bound
2022-03-15 09:46:40 -04:00
M. Anthony Aiello
c087aac77b Merge pull request #37 from joffreyhuguet/silver_level_proof_algebra_tree
Silver level proof algebra tree
2021-10-28 15:14:41 -04:00
Joffrey Huguet
7bbdaa3c3e Update session files and proof testsuite 2021-10-25 17:40:25 +02:00
Joffrey Huguet
37be0e7333 Merge pull request #36 from AdaCore/integration
Integration
2021-10-25 16:58:58 +02:00
Joffrey Huguet
7fcf0280fc Silver-level proof of algebra tree generation 2021-10-22 12:51:01 +02:00
M. Anthony Aiello
77da5a56aa Update the install scripts for CE21 (#35)
We now use CE21 rather than CE20.
2021-10-21 11:23:48 -04:00
Joffrey Huguet
f8859bde87 Merge pull request #29 from joffreyhuguet/improve_proof_testsuite
Improve run-proofs.py to allow to run on non-replay mode, to easily rewrite session files
2021-10-21 17:13:52 +02:00
Joffrey Huguet
bf2ca34d75 Complete silver-level proof of main functionality of Assignment Tree Branch Bound 2021-10-21 15:38:38 +02:00
Joffrey Huguet
61b336ab7c Update session files and testsuite 2021-10-21 15:38:19 +02:00
Joffrey Huguet
a04e130b3b Complete silver-level proof of main functionality of Assignment Tree Branch Bound 2021-10-21 14:27:02 +02:00
Joffrey Huguet
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.
2021-10-21 14:26:19 +02:00
Joffrey Huguet
99054911e4 Merge branch 'integration' into improve_proof_testsuite 2021-10-20 10:15:00 +02:00
Joffrey Huguet
f8ee438e26 Merge pull request #34 from joffreyhuguet/update_to_community2021
Update Actions to use Community Edition 2021; fix testsuites
2021-10-19 17:16:04 +02:00
Pat Rogers
0192696235 Merge pull request #32 from pat-rogers/integration
fix problem with static call to non-abstract subprogram... highlighted by Community Edition 2021
2021-10-19 09:34:45 -05:00
rogers
e88b1d0678 fix problem with static call to non-abstract subprogram... highlighted by Community Edition 2021 2021-10-18 16:41:43 -05:00
Joffrey Huguet
ea0e4a2fd9 Improve run-proofs.py to allow to run on non-replay mode, to easily rewrite session files 2021-09-10 14:48:45 +02:00
lhumphrey
9bbf1e6c16 Merge pull request #35 from AdaCore/integration
Fix errors for RunLmcpGen.py (#30)
2021-08-25 15:57:24 -04:00
M. Anthony Aiello
321f0bfcd8 Fix errors for RunLmcpGen.py (#30)
RunLmcpGen.py no longer worked; the paths returned by the `uxas.paths`
python module were not correct; they were relative to the parent
directory of the OpenUxAS repo, not to the OpenUxAS repo itself.

Most likely, this occurred because of some change in the way the module
was installed in the python venv. To make this more robust, the paths
are now computed different: they look explicitly for the parent of the
.vpython directory itself.

Additionally, there was a possibility that the computation of the
`base_env` in RunLmcpGen.py would fail: the loop indexing requires that
the length of the array mod 2 be zero. This is now encoded explicitly.
2021-08-25 15:16:51 -04:00
Joffrey Huguet
75b2dff91d Adjust variables in Ada code to run the demos properly 2021-08-19 11:15:09 +02:00
Joffrey Huguet
ee500fc6b8 Use GNAT Community Edition 2021 in GitHub Actions 2021-07-28 09:32:48 +02:00
Joffrey Huguet
57319a5a39 Update session files for CE2021 2021-07-26 17:47:38 +02:00
Joffrey Huguet
806867534f Update files to prove with CE2021 2021-07-26 16:53:41 +02:00
lhumphrey
1df751b817 Merge pull request #32 from AdaCore/integration
Implement greedy traversal of the "search tree" in the Ada ATBB
2021-07-07 13:32:18 -04:00