GitHub - jonnybest/Alloy2RelSMT: This is Alloy2RelSMT, a converter. It translates Alloy models into SMT files with a specific relational theory.

This repository has been archived by the owner on Jan 26, 2018. It is now read-only.

jonnybest / Alloy2RelSMT Public archive

Notifications You must be signed in to change notification settings
Fork 0
Star 1

This is Alloy2RelSMT, a converter. It translates Alloy models into SMT files with a specific relational theory.

Notifications

Name		Name	Last commit message	Last commit date
Latest commit History 386 Commits
.settings		.settings
edu/mit/csail/sdg/alloy4/parser		edu/mit/csail/sdg/alloy4/parser
res		res
rule_generation		rule_generation
src		src
.classpath		.classpath
.gitignore		.gitignore
.project		.project
README		README
alloy2relsmt		alloy2relsmt
build.xml		build.xml

Repository files navigation

Alloy2RelSMT
---------

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

## Command line options
alloy2relsmt <alloyfile> <smtfile> [-f|--force] [--finite=<Sig1>[,<Sig2>,…]] [-nre]
	<alloyfile>			denotes an input file
	<smtfile>			name of the output file

Optional:
	--force, -f 					forces overwriting the output file if exists
	--finite=<Sig1>[,<Sig2>,…]		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.