Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Add TLA+ output of a Cubicle model with -tla option. #2

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
Open

Add TLA+ output of a Cubicle model with -tla option. #2

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 5 additions & 3 deletions Makefile.in
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -48,7 +48,7 @@ INCLUDES = $(INCLPATHS) $(Z3CCFLAGS)
BFLAGS = -dtypes -g $(INCLUDES) -annot
OFLAGS = -dtypes -g $(INCLUDES) -annot

REQBIB=nums.cma unix.cma functory.cma
REQBIB=nums.cma unix.cma functory.cma str.cma

ifeq ($(Z3LIB),)
BIBBYTE=$(REQBIB)
Expand Down Expand Up @@ -119,6 +119,7 @@ CMO = version.cmo options.cmo \
pre.cmo forward.cmo enumerative.cmo \
muparser_globals.cmo muparser.cmo mulexer.cmo murphi.cmo \
approx.cmo \
tla.cmo \
stats.cmo bwd.cmo brab.cmo typing.cmo trace.cmo main.cmo

CMX = $(CMO:.cmo=.cmx)
Expand All @@ -139,7 +140,7 @@ $(NAME).opt: $(MAINCMX)
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLOPT) $(OFLAGS) -o $@ $(BIBOPT) $^

VERSION=1.1.2
VERSION=1.1.3
VERSION_STR=$(shell command -v git > /dev/null && git describe --tags || echo "$(VERSION)")

version.ml: config.status
Expand Down Expand Up @@ -305,7 +306,8 @@ FILES = approx.ml approx.mli ast.mli ptree.mli ptree.ml\
parser.mly pre.ml pre.mli pretty.ml pretty.mli prover.ml prover.mli\
safety.ml safety.mli stats.ml stats.mli trace.ml trace.mli\
types.ml types.mli typing.ml typing.mli util.ml util.mli\
variable.ml variable.mli version.ml
variable.ml variable.mli version.ml \
tla.mli tla.ml

EXAMPLES = bakery.cub dijkstra.cub distrib_channels.cub jml.cub\
ricart_abdulla.cub szymanski_at.cub berkeley.cub flash_eager.cub\
Expand Down
1 change: 1 addition & 0 deletions main.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -63,6 +63,7 @@ let _ =
let s = Parser.system Lexer.token lb in
let system = Typing.system s in
if type_only then exit 0;
if tla then begin Tla.print stdout s; exit 0; end;
if refine_universal then
printf "@{<b>@{<fg_yellow>Warning@} !@}\nUniversal guards refinement \
is an experimental feature. Use at your own risks.\n@.";
Expand Down
4 changes: 4 additions & 0 deletions options.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -24,6 +24,8 @@ let js_mode = ref false
let usage = "usage: cubicle file.cub"
let file = ref "_stdin"

let tla = ref false

let max_proc = ref 10
let type_only = ref false
let maxrounds = ref 100
Expand Down Expand Up @@ -122,6 +124,7 @@ let specs =
[ "-version", Arg.Unit show_version, " prints the version number";
"-quiet", Arg.Set quiet, " do not output search trace";
"-nocolor", Arg.Set nocolor, " disable colors in ouptut";
"-tla", Arg.Set tla, " output TLA+ module";
"-type-only", Arg.Set type_only, " stop after typing";
"-max-procs", Arg.Set_int max_proc,
"<nb> max number of processes to introduce (default 10)";
Expand Down Expand Up @@ -218,6 +221,7 @@ let cin =
| Some f -> file := f ; open_in f
| None -> stdin

let tla = !tla
let type_only = !type_only
let maxrounds = !maxrounds
let maxnodes = !maxnodes
Expand Down
2 changes: 2 additions & 0 deletions options.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -24,6 +24,8 @@ type solver = AltErgo | Z3
val file : string
val cin : in_channel

val tla : bool

val max_proc : int
val type_only : bool
val maxrounds : int
Expand Down
Loading