\pagebreak
The formal system of the RLA Tool is specified in a Literate PVS
specification in specs/pvs/corla.pvs
. We will integrate the two
documents for final system delivery. See the working draft, generated
from that formal specification, in
our
GitHub repository.
To be written.
To be written.
To be written.
To be written.