We have developed a domain-specific language with an appearance resembling other modeling language such as Murphi and TCL+, that is specific to representing API state transitions and is run through a compiler to automatically output:
* MediaWiki-formatted documentation (using LaTex features)
* if desired: parse tree, pretty-printed (source language, minus comments) version.

Ideally it would also be able to output:
* Golden executable
* Could it generate test cases automatically?
* Keep the comments from the source to show in the documentation output

[[FormalSpec.g]] -- ANTLR grammar of our formal specification language

The complete [https://github.com/ericmercer/4M framework] for our modeling system of the MCAPI API is located on [http://github.com Github]. We also have a separate framework for translating MCAPI executions traces into [https://github.com/ericmercer/MP-trace-language SMT problems].

[[MCAPI|Back]]

== MCAPI Formalization ==

Here is our work-in-progress on formalizing the MCAPI specification using the "Formal Spec" language.

[[Thoughts on Murphi Conversion]]

=== Init/Finalize, Endpoint operations ===

* [[mcapi_endpoints.fspec]] -- fspec file
* [[mcapi_endpoints_doc]] -- generated documentation

=== Connectionless operations ===

* [[mcapi_connectionless.fspec]] -- fspec file
* [[mcapi_connectionless_doc]] -- generated documentation
* [[mcapi.fspec]] -- This is the FSpec file used in the working version of the GEM

Download the complete [https://github.com/ericmercer/4M framework] for our modeling system of the MCAPI API is located on [http://github.com Github]. We also have a separate framework for translating MCAPI executions traces into [https://github.com/ericmercer/MP-trace-language SMT problems].

[[MCAPI|Back]]