search

jonnybest / Alloy2RelSMT

This is Alloy2RelSMT, a converter. It translates Alloy models into SMT files with a specific relational theory.
1 stars 0 forks source link

readme

Alloy2RelSMT

This applications translates a given Alloy model to first-order logic in SMT.

Command line options

alloy2relsmt [-f|--force] [--finite=[,,…]] [-nre]

denotes an input file name of the output file Optional: --force, -f forces overwriting the output file if exists --finite=[,,…] assume that signatures Sig1, Sig2,… are finite --relationalequality, -re writes "equality" formulas as two subset expressions [default] --no-relationalequality, -nre use = operator for relational expressions instead of subset ----------------------------- Original Readme ----------------------------- Alloy2KeY --------- Translate an Alloy model to First-Order logic in KeY syntax. Compilation: ------------ To compile Alloy2KeY, run ant within the project's top-level directory. This will compile everything to the build directory. Running Alloy2KeY: ------------------ Use the alloy2key script located in the project's top-level directory to translate an alloy specification. alloy2key takes the input Alloy model as first command line argument. A second (optional) argument defines the output file. For details call the program without any arguments.