Permalink
Browse files

Merge branch 'release/0.0.5'

  • Loading branch information...
mwolf76 committed Dec 28, 2016
2 parents 87bbebc + 2a18229 commit c62d1d2b0718c6ee7cb21e6c81a76199d421ccb3
Showing with 2,130 additions and 49,548 deletions.
  1. +2 −2 .gitignore
  2. +68 −65 Makefile.am
  3. +31 −31 README
  4. +8 −9 configure.ac
  5. +5 −0 debian/changelog
  6. +1 −0 debian/compat
  7. +25 −0 debian/control
  8. +27 −0 debian/copyright
  9. +3 −0 debian/rules
  10. +1 −0 debian/source/format
  11. +1 −0 debian/yasmv.manpages
  12. +2 −2 examples/{input → automation}/automation.smv
  13. +1 −0 examples/{input/automation.cmd → automation/commands}
  14. +3 −2 examples/{ → cannibals}/cannibals.smv
  15. +1 −0 examples/{cannibals.cmd → cannibals/commands}
  16. +1 −0 examples/{hanoi.cmd → ferryman/commands}
  17. +4 −7 examples/{ → ferryman}/ferryman.smv
  18. +2 −1 examples/{input/fibonacci.cmd → fibonacci/commands}
  19. +3 −1 examples/{input → fibonacci}/fibonacci.smv
  20. +1 −0 examples/{ferryman.cmd → hanoi/commands}
  21. +2 −1 examples/{ → hanoi}/hanoi3.smv
  22. +3 −0 examples/{ → hanoi}/hanoi4.smv
  23. +3 −0 examples/{ → hanoi}/hanoi5.smv
  24. +1 −0 examples/{koenisberg.cmd → herschel/commands}
  25. +2 −1 examples/{ → herschel}/herschel.smv
  26. +1 −0 examples/{herschel.cmd → koenisberg/commands}
  27. +2 −1 examples/{ → koenisberg}/koenisberg.smv
  28. +1 −0 examples/maze/{maze.cmd → commands}
  29. +1 −1 examples/maze/solvable8x8.smv
  30. +3 −3 examples/maze/unsolvable8x8.smv
  31. +1 −0 examples/{input/prime.cmd → primes/commands}
  32. +2 −2 examples/{input/prime.smv → primes/primes.smv}
  33. +0 −3 examples/tic-tac-toe.cmd
  34. +4 −0 examples/tic-tac-toe/commands
  35. +6 −1 examples/{ → tic-tac-toe}/tic-tac-toe.smv
  36. +1 −0 examples/{input/vending.cmd → vending/commands}
  37. +2 −1 examples/{input → vending}/vending.smv
  38. +164 −0 man/yasmv.1
  39. +6 −7 microcode/README
  40. +16 −5 setup.sh
  41. +2 −3 src/3rdparty/Makefile.am
  42. +8 −0 src/3rdparty/ezlogger/Makefile.am
  43. +0 −9 src/3rdparty/jsoncpp/Makefile.am
  44. +0 −264 src/3rdparty/jsoncpp/json-forwards.hh
  45. +0 −3,752 src/3rdparty/jsoncpp/json.cc
  46. +0 −1,976 src/3rdparty/jsoncpp/json.hh
  47. +1 −1 src/Makefile.am
  48. +3 −1 src/algorithms/Makefile.am
  49. +7 −12 src/algorithms/base.cc
  50. +1 −0 src/algorithms/base.hh
  51. +8 −5 src/algorithms/bmc/Makefile.am
  52. +38 −39 src/algorithms/bmc/backward.cc
  53. +19 −17 src/algorithms/bmc/{classes.cc → bmc.cc}
  54. +28 −7 src/algorithms/bmc/bmc.hh
  55. +0 −55 src/algorithms/bmc/classes.hh
  56. +33 −32 src/algorithms/bmc/forward.cc
  57. +26 −145 src/algorithms/bmc/witness.cc
  58. +5 −13 src/algorithms/bmc/witness.hh
  59. +2 −1 src/algorithms/fsm/Makefile.am
  60. +0 −47 src/algorithms/init.cc
  61. +2 −1 src/algorithms/ltl/Makefile.am
  62. +1 −3 src/algorithms/sim/Makefile.am
  63. +8 −2 src/algorithms/sim/simulation.cc
  64. +14 −5 src/algorithms/sim/witness.cc
  65. +2 −1 src/cmd/Makefile.am
  66. +5 −3 src/cmd/cmd.cc
  67. +2 −3 src/cmd/command.hh
  68. +27 −17 src/cmd/commands/Makefile.am
  69. +2 −1 src/cmd/commands/add_init.cc
  70. +2 −1 src/cmd/commands/add_invar.cc
  71. +2 −1 src/cmd/commands/add_trans.cc
  72. +2 −1 src/cmd/commands/clear.cc
  73. +9 −7 src/cmd/commands/commands.cc
  74. +4 −0 src/cmd/commands/commands.hh
  75. +3 −1 src/cmd/commands/dump_model.cc
  76. +150 −52 src/cmd/commands/dump_trace.cc
  77. +31 −1 src/cmd/commands/dump_trace.hh
  78. +3 −2 src/cmd/commands/get.cc
  79. +2 −1 src/cmd/commands/help.cc
  80. +0 −73 src/cmd/commands/if.cc
  81. +0 −60 src/cmd/commands/if.hh
  82. +3 −1 src/cmd/commands/list_traces.cc
  83. +1 −1 src/cmd/commands/quit.cc
  84. +1 −0 src/cmd/commands/quit.hh
  85. +3 −1 src/cmd/commands/read_model.cc
  86. +2 −1 src/cmd/commands/set.cc
  87. +7 −4 src/cmd/commands/time.cc
  88. +0 −68 src/cmd/commands/while.cc
  89. +0 −59 src/cmd/commands/while.hh
  90. +0 −4 src/cmd/interpreter.cc
  91. +1 −11 src/cmd/interpreter.hh
  92. +0 −67 src/cmd/job.cc
  93. +0 −73 src/cmd/job.hh
  94. +12 −5 src/common/Makefile.am
  95. +0 −30 src/common/tokens.hh
  96. +46 −44 src/dd/Makefile.am
  97. +0 −6,776 src/dd/cudd-2.5.0/cudd/doc/cudd.doc
  98. BIN src/dd/cudd-2.5.0/cudd/doc/cudd.ps
  99. +0 −3,114 src/dd/cudd-2.5.0/cudd/doc/cuddAllAbs.html
  100. +0 −13 src/dd/cudd-2.5.0/cudd/doc/cuddAllByFile.html
  101. +0 −13 src/dd/cudd-2.5.0/cudd/doc/cuddAllByFunc.html
  102. +0 −15,754 src/dd/cudd-2.5.0/cudd/doc/cuddAllDet.html
  103. +0 −4,876 src/dd/cudd-2.5.0/cudd/doc/cuddAllFile.html
  104. +0 −33 src/dd/cudd-2.5.0/cudd/doc/cuddDesc.html
  105. +0 −14 src/dd/cudd-2.5.0/cudd/doc/cuddExt.html
  106. +0 −1,415 src/dd/cudd-2.5.0/cudd/doc/cuddExtAbs.html
  107. +0 −4,450 src/dd/cudd-2.5.0/cudd/doc/cuddExtDet.html
  108. +0 −30 src/dd/cudd-2.5.0/cudd/doc/cuddIntro.css
  109. +0 −219 src/dd/cudd-2.5.0/cudd/doc/cuddIntro.html
  110. +0 −18 src/dd/cudd-2.5.0/cudd/doc/cuddTitle.html
  111. +0 −109 src/dd/cudd-2.5.0/cudd/doc/footnode.html
  112. BIN src/dd/cudd-2.5.0/cudd/doc/icons/blueball.png
  113. BIN src/dd/cudd-2.5.0/cudd/doc/icons/ch_beg_r.png
  114. BIN src/dd/cudd-2.5.0/cudd/doc/icons/ch_begin.png
  115. BIN src/dd/cudd-2.5.0/cudd/doc/icons/ch_del_r.png
  116. BIN src/dd/cudd-2.5.0/cudd/doc/icons/ch_delet.png
  117. BIN src/dd/cudd-2.5.0/cudd/doc/icons/ch_end.png
  118. BIN src/dd/cudd-2.5.0/cudd/doc/icons/ch_end_r.png
  119. BIN src/dd/cudd-2.5.0/cudd/doc/icons/contents.png
  120. BIN src/dd/cudd-2.5.0/cudd/doc/icons/crossref.png
  121. BIN src/dd/cudd-2.5.0/cudd/doc/icons/footnote.png
  122. BIN src/dd/cudd-2.5.0/cudd/doc/icons/greenball.png
  123. BIN src/dd/cudd-2.5.0/cudd/doc/icons/image.png
  124. BIN src/dd/cudd-2.5.0/cudd/doc/icons/index.png
  125. BIN src/dd/cudd-2.5.0/cudd/doc/icons/next.png
  126. BIN src/dd/cudd-2.5.0/cudd/doc/icons/next_g.png
  127. BIN src/dd/cudd-2.5.0/cudd/doc/icons/nx_grp.png
  128. BIN src/dd/cudd-2.5.0/cudd/doc/icons/nx_grp_g.png
  129. BIN src/dd/cudd-2.5.0/cudd/doc/icons/orangeball.png
  130. BIN src/dd/cudd-2.5.0/cudd/doc/icons/pinkball.png
  131. BIN src/dd/cudd-2.5.0/cudd/doc/icons/prev.png
  132. BIN src/dd/cudd-2.5.0/cudd/doc/icons/prev_g.png
  133. BIN src/dd/cudd-2.5.0/cudd/doc/icons/purpleball.png
  134. BIN src/dd/cudd-2.5.0/cudd/doc/icons/pv_grp.png
  135. BIN src/dd/cudd-2.5.0/cudd/doc/icons/pv_grp_g.png
  136. BIN src/dd/cudd-2.5.0/cudd/doc/icons/redball.png
  137. BIN src/dd/cudd-2.5.0/cudd/doc/icons/up.png
  138. BIN src/dd/cudd-2.5.0/cudd/doc/icons/up_g.png
  139. BIN src/dd/cudd-2.5.0/cudd/doc/icons/whiteball.png
  140. BIN src/dd/cudd-2.5.0/cudd/doc/icons/yellowball.png
  141. BIN src/dd/cudd-2.5.0/cudd/doc/img1.png
  142. BIN src/dd/cudd-2.5.0/cudd/doc/img10.png
  143. BIN src/dd/cudd-2.5.0/cudd/doc/img11.png
  144. BIN src/dd/cudd-2.5.0/cudd/doc/img12.png
  145. BIN src/dd/cudd-2.5.0/cudd/doc/img13.png
  146. BIN src/dd/cudd-2.5.0/cudd/doc/img14.png
  147. BIN src/dd/cudd-2.5.0/cudd/doc/img15.png
  148. BIN src/dd/cudd-2.5.0/cudd/doc/img16.png
  149. BIN src/dd/cudd-2.5.0/cudd/doc/img17.png
  150. BIN src/dd/cudd-2.5.0/cudd/doc/img18.png
  151. BIN src/dd/cudd-2.5.0/cudd/doc/img19.png
  152. BIN src/dd/cudd-2.5.0/cudd/doc/img2.png
  153. BIN src/dd/cudd-2.5.0/cudd/doc/img20.png
  154. BIN src/dd/cudd-2.5.0/cudd/doc/img21.png
  155. BIN src/dd/cudd-2.5.0/cudd/doc/img22.png
  156. BIN src/dd/cudd-2.5.0/cudd/doc/img3.png
  157. BIN src/dd/cudd-2.5.0/cudd/doc/img4.png
  158. BIN src/dd/cudd-2.5.0/cudd/doc/img5.png
  159. BIN src/dd/cudd-2.5.0/cudd/doc/img6.png
  160. BIN src/dd/cudd-2.5.0/cudd/doc/img7.png
  161. BIN src/dd/cudd-2.5.0/cudd/doc/img8.png
  162. BIN src/dd/cudd-2.5.0/cudd/doc/img9.png
  163. +0 −219 src/dd/cudd-2.5.0/cudd/doc/index.html
  164. +0 −174 src/dd/cudd-2.5.0/cudd/doc/node1.html
  165. +0 −175 src/dd/cudd-2.5.0/cudd/doc/node2.html
  166. +0 −1,637 src/dd/cudd-2.5.0/cudd/doc/node3.html
  167. +0 −1,165 src/dd/cudd-2.5.0/cudd/doc/node4.html
  168. +0 −130 src/dd/cudd-2.5.0/cudd/doc/node5.html
  169. +0 −132 src/dd/cudd-2.5.0/cudd/doc/node6.html
  170. +0 −195 src/dd/cudd-2.5.0/cudd/doc/node7.html
  171. +0 −848 src/dd/cudd-2.5.0/cudd/doc/node8.html
  172. +28 −43 src/dd/dd_walker.cc
  173. +4 −7 src/dd/dd_walker.hh
  174. +5 −2 src/enc/Makefile.am
  175. +1 −1 src/enc/enc.hh
  176. +2 −1 src/env/Makefile.am
  177. +2 −1 src/expr/Makefile.am
  178. +1 −1 src/expr/expr_mgr.hh
  179. +2 −4 src/expr/printer/Makefile.am
  180. +1 −5 src/expr/printer/leaf.cc
  181. +3 −7 src/expr/walker/Makefile.am
  182. +50 −0 src/expr/walker/exceptions.cc
  183. +4 −14 src/expr/walker/exceptions.hh
  184. +24 −28 src/main.cc
  185. +11 −6 src/model/Makefile.am
  186. +8 −5 src/model/analyzer/Makefile.am
  187. +3 −2 src/model/analyzer/analyzer.cc
  188. +53 −5 src/model/analyzer/walker.cc
  189. +3 −1 src/model/compiler/Makefile.am
  190. +18 −5 src/model/compiler/exceptions.cc
  191. +14 −1 src/model/compiler/exceptions.hh
  192. +4 −4 src/model/compiler/leaves.cc
  193. +1 −1 src/model/compiler/walker.cc
  194. +3 −0 src/model/exceptions.hh
  195. +9 −14 src/{algorithms/init.hh → model/helpers.cc}
  196. +115 −0 src/model/model.cc
  197. +29 −6 src/model/model.hh
  198. +30 −15 src/model/model_mgr.cc
  199. +5 −8 src/model/model_mgr.hh
  200. +4 −4 src/model/model_resolver.cc
  201. +48 −93 src/model/{classes.cc → module.cc}
  202. +35 −46 src/model/{classes.hh → module.hh}
  203. +3 −2 src/model/preprocessor/Makefile.am
  204. +1 −0 src/model/preprocessor/preprocessor.cc
  205. +1 −0 src/model/preprocessor/preprocessor.hh
  206. +15 −9 src/model/symb_iter.cc
  207. +3 −2 src/model/type_checker/Makefile.am
  208. +2 −0 src/model/type_checker/type_checker.cc
  209. +8 −1 src/model/typedefs.hh
  210. +17 −0 src/opts/Makefile.am
  211. 0 src/{ → opts}/opts_mgr.cc
  212. 0 src/{ → opts}/opts_mgr.hh
  213. +7 −7 src/parse.cc
  214. +8 −5 src/parser/Makefile.am
  215. +8 −0 src/parser/grammars/Makefile.am
  216. +0 −3 src/parser/grammars/grammar.hh
  217. +54 −47 src/parser/grammars/smv.g
  218. +5 −5 src/sat/Makefile.am
  219. +0 −31 src/sat/cnf.cc
  220. +87 −47 src/sat/cnf_nocut.cc
  221. +23 −3 src/sat/cnf_registry.cc
  222. +124 −100 src/sat/cnf_singlecut.cc
  223. +8 −1 src/sat/engine.hh
  224. +17 −12 src/sat/exceptions.cc
  225. +1 −4 src/sat/exceptions.hh
  226. +88 −78 src/sat/inlining.cc
  227. +2 −0 src/sat/inlining.hh
  228. +1 −9 src/sat/sat.hh
  229. +2 −2 src/sat/time_mapper.cc
  230. +4 −4 src/sat/typedefs.hh
  231. +4 −4 src/symb/Makefile.am
  232. +5 −3 src/symb/classes.cc
  233. +10 −2 src/symb/classes.hh
  234. +5 −0 src/symb/proxy.hh
  235. +1 −1 src/symb/{iter.cc → symb_iter.cc}
  236. +3 −13 src/symb/{iter.hh → symb_iter.hh}
  237. +0 −46 src/symb/symbol.hh
  238. +4 −1 src/symb/typedefs.hh
  239. +6 −5 src/type/Makefile.am
  240. +10 −11 src/type/classes.hh
  241. +35 −6 src/type/exceptions.cc
  242. +5 −32 src/type/exceptions.hh
  243. +0 −3 src/type/helpers.hh
  244. +0 −3 src/type/printers.hh
  245. +0 −3 src/type/type.hh
  246. +4 −1 src/type/type_mgr.cc
  247. +0 −2 src/type/type_mgr.hh
  248. +6 −3 src/type/type_resolver.cc
  249. +0 −3 src/type/typedefs.hh
  250. +3 −2 src/utils/Makefile.am
  251. +2 −3 src/utils/misc.hh
  252. +20 −35 src/utils/variant.cc
  253. +1 −2 src/utils/variant.hh
  254. +10 −5 src/witness/Makefile.am
  255. +3 −3 src/witness/internals.cc
  256. +1 −3 src/witness/out/Makefile.am
  257. +18 −5 src/witness/witness.cc
  258. +4 −0 src/witness/witness.hh
  259. +14 −0 src/witness/witness_mgr.cc
  260. +2 −4 src/witness/witness_mgr.hh
  261. 0 {src/model → testing}/test_compiler.cc
  262. 0 {src/dd → testing}/test_dd.cc
  263. 0 {src/enc → testing}/test_enc.cc
  264. 0 {src/expr → testing}/test_expr.cc
  265. 0 {src/parser → testing}/test_parser.cc
  266. 0 {src/type → testing}/test_type.cc
  267. 0 {src → testing}/tests.cc
  268. +3 −0 tools/build-deb.sh
  269. +3 −3 tools/ucodegen/ucodegen.py
  270. 0 gnusmv.pc.in → yasmv.pc.in
View
@@ -15,11 +15,11 @@ smvLexer*
smvParser*
helpers/
libtool
-gnusmv.pc
INSTALL
TAGS
.timestamp
smv.tokens
stamp-h1
-tests
+yasmv.pc
yasmv
+yasmv_tests
View
@@ -25,83 +25,86 @@ AM_CPPFLAGS = -I$(top_srcdir)/src -I$(top_srcdir)/src/dd \
-I$(top_srcdir)/src/dd/cudd-2.5.0/util \
-I$(top_srcdir)/src/dd/cudd-2.5.0/obj
-bin_PROGRAMS = yasmv tests
+bin_PROGRAMS = yasmv
+EXTRA_PROGRAMS = yasmv_tests
+dist_pkgdata_DATA = microcode/*
# tags target helper (uses exuberant ctags)
tags:
@ctags -Ref TAGS $(top_srcdir)
-yasmv_SOURCES = src/opts_mgr.cc src/main.cc src/parse.cc
+yasmv_SOURCES = src/main.cc src/parse.cc
yasmv_LDADD = $(top_builddir)/src/parser/libparser.la \
- $(top_builddir)/src/cmd/libcmd.la \
- $(top_builddir)/src/cmd/commands/libcommands.la \
- $(top_builddir)/src/algorithms/bmc/libbmc.la \
- $(top_builddir)/src/algorithms/fsm/libfsm.la \
- $(top_builddir)/src/algorithms/ltl/libltl.la \
- $(top_builddir)/src/algorithms/sim/libsim.la \
- $(top_builddir)/src/algorithms/libalgorithms.la \
- $(top_builddir)/src/model/libmodel.la \
- $(top_builddir)/src/model/compiler/libcompiler.la \
- $(top_builddir)/src/enc/libenc.la \
- $(top_builddir)/src/env/libenv.la \
- $(top_builddir)/src/model/analyzer/libanalyzer.la \
- $(top_builddir)/src/model/type_checker/libtype_checker.la \
- $(top_builddir)/src/model/preprocessor/libpreprocessor.la \
- $(top_builddir)/src/expr/libexpr.la \
- $(top_builddir)/src/expr/walker/libexpr_walker.la \
- $(top_builddir)/src/expr/printer/libprinter.la \
- $(top_builddir)/src/type/libtype.la \
- $(top_builddir)/src/symb/libsymb.la \
- $(top_builddir)/src/utils/libutils.la \
- $(top_builddir)/src/witness/libwitness.la \
- $(top_builddir)/src/sat/libsat.la \
- $(top_builddir)/src/common/libcommon.la \
+ $(top_builddir)/src/cmd/libcmd.la \
+ $(top_builddir)/src/cmd/commands/libcommands.la \
+ $(top_builddir)/src/algorithms/bmc/libbmc.la \
+ $(top_builddir)/src/algorithms/fsm/libfsm.la \
+ $(top_builddir)/src/algorithms/ltl/libltl.la \
+ $(top_builddir)/src/algorithms/sim/libsim.la \
+ $(top_builddir)/src/algorithms/libalgorithms.la \
+ $(top_builddir)/src/model/libmodel.la \
+ $(top_builddir)/src/model/compiler/libcompiler.la \
+ $(top_builddir)/src/enc/libenc.la \
+ $(top_builddir)/src/env/libenv.la \
+ $(top_builddir)/src/model/analyzer/libanalyzer.la \
+ $(top_builddir)/src/model/type_checker/libtype_checker.la \
+ $(top_builddir)/src/model/preprocessor/libpreprocessor.la \
+ $(top_builddir)/src/expr/libexpr.la \
+ $(top_builddir)/src/expr/walker/libexpr_walker.la \
+ $(top_builddir)/src/expr/printer/libprinter.la \
+ $(top_builddir)/src/type/libtype.la \
+ $(top_builddir)/src/symb/libsymb.la \
+ $(top_builddir)/src/utils/libutils.la \
+ $(top_builddir)/src/witness/libwitness.la \
+ $(top_builddir)/src/sat/libsat.la \
+ $(top_builddir)/src/common/libcommon.la \
+ $(top_builddir)/src/opts/libopts.la \
\
- $(top_builddir)/src/dd/libcudd.la -lminisat -lantlr3c \
- $(top_builddir)/src/3rdparty/jsoncpp/libjson.la \
- $(BOOST_PROGRAM_OPTIONS_LIBS) $(BOOST_FILESYSTEM_LIBS) \
- $(BOOST_THREAD_LIBS) $(BOOST_CHRONO_LIBS)
+ $(top_builddir)/src/dd/libcudd.la -lminisat -lantlr3c \
+ -ljsoncpp $(BOOST_PROGRAM_OPTIONS_LIBS) \
+ $(BOOST_FILESYSTEM_LIBS) $(BOOST_THREAD_LIBS) \
+ $(BOOST_CHRONO_LIBS)
yasmv_LDFLAGS = $(BOOST_REGEX_LDFLAGS) -L/usr/local/lib
-tests_SOURCES = src/opts_mgr.cc src/parse.cc src/tests.cc \
- src/expr/test_expr.cc src/parser/test_parser.cc \
- src/type/test_type.cc src/dd/test_dd.cc src/enc/test_enc.cc \
- src/model/test_compiler.cc
+yasmv_tests_SOURCES = src/parse.cc testing/tests.cc \
+ testing/test_expr.cc testing/test_parser.cc \
+ testing/test_type.cc testing/test_dd.cc \
+ testing/test_enc.cc testing/test_compiler.cc
-tests_LDADD = $(top_builddir)/src/parser/libparser.la \
- $(top_builddir)/src/cmd/libcmd.la \
- $(top_builddir)/src/cmd/commands/libcommands.la \
- $(top_builddir)/src/algorithms/bmc/libbmc.la \
- $(top_builddir)/src/algorithms/fsm/libfsm.la \
- $(top_builddir)/src/algorithms/ltl/libltl.la \
- $(top_builddir)/src/algorithms/sim/libsim.la \
- $(top_builddir)/src/algorithms/libalgorithms.la \
- $(top_builddir)/src/model/libmodel.la \
- $(top_builddir)/src/model/compiler/libcompiler.la \
- $(top_builddir)/src/enc/libenc.la \
- $(top_builddir)/src/env/libenv.la \
- $(top_builddir)/src/model/analyzer/libanalyzer.la \
- $(top_builddir)/src/model/type_checker/libtype_checker.la \
- $(top_builddir)/src/model/preprocessor/libpreprocessor.la \
- $(top_builddir)/src/expr/libexpr.la \
- $(top_builddir)/src/expr/walker/libexpr_walker.la \
- $(top_builddir)/src/expr/printer/libprinter.la \
- $(top_builddir)/src/type/libtype.la \
- $(top_builddir)/src/symb/libsymb.la \
- $(top_builddir)/src/utils/libutils.la \
- $(top_builddir)/src/witness/libwitness.la \
- $(top_builddir)/src/sat/libsat.la \
- $(top_builddir)/src/common/libcommon.la \
- \
- $(top_builddir)/src/dd/libcudd.la -lminisat -lantlr3c \
- $(top_builddir)/src/3rdparty/jsoncpp/libjson.la \
- $(BOOST_PROGRAM_OPTIONS_LIBS) $(BOOST_FILESYSTEM_LIBS) \
- $(BOOST_THREAD_LIBS) $(BOOST_CHRONO_LIBS) \
- -lboost_unit_test_framework
+yasmv_tests_LDADD = $(top_builddir)/src/parser/libparser.la \
+ $(top_builddir)/src/cmd/libcmd.la \
+ $(top_builddir)/src/cmd/commands/libcommands.la \
+ $(top_builddir)/src/algorithms/bmc/libbmc.la \
+ $(top_builddir)/src/algorithms/fsm/libfsm.la \
+ $(top_builddir)/src/algorithms/ltl/libltl.la \
+ $(top_builddir)/src/algorithms/sim/libsim.la \
+ $(top_builddir)/src/algorithms/libalgorithms.la \
+ $(top_builddir)/src/model/libmodel.la \
+ $(top_builddir)/src/model/compiler/libcompiler.la \
+ $(top_builddir)/src/enc/libenc.la \
+ $(top_builddir)/src/env/libenv.la \
+ $(top_builddir)/src/model/analyzer/libanalyzer.la \
+ $(top_builddir)/src/model/type_checker/libtype_checker.la \
+ $(top_builddir)/src/model/preprocessor/libpreprocessor.la \
+ $(top_builddir)/src/expr/libexpr.la \
+ $(top_builddir)/src/expr/walker/libexpr_walker.la \
+ $(top_builddir)/src/expr/printer/libprinter.la \
+ $(top_builddir)/src/type/libtype.la \
+ $(top_builddir)/src/symb/libsymb.la \
+ $(top_builddir)/src/utils/libutils.la \
+ $(top_builddir)/src/witness/libwitness.la \
+ $(top_builddir)/src/sat/libsat.la \
+ $(top_builddir)/src/common/libcommon.la \
+ $(top_builddir)/src/opts/libopts.la \
+ \
+ $(top_builddir)/src/dd/libcudd.la -lminisat -lantlr3c \
+ -ljsoncpp $(BOOST_PROGRAM_OPTIONS_LIBS) \
+ $(BOOST_FILESYSTEM_LIBS) $(BOOST_THREAD_LIBS) \
+ $(BOOST_CHRONO_LIBS) -lboost_unit_test_framework
-tests_LDFLAGS = $(BOOST_REGEX_LDFLAGS) -L/usr/local/lib
+yasmv_tests_LDFLAGS = $(BOOST_REGEX_LDFLAGS) -L/usr/local/lib
pkgconfdir = $(libdir)/pkgconfig
-pkgconf_DATA = gnusmv.pc
+pkgconf_DATA = yasmv.pc
View
62 README
@@ -1,37 +1,38 @@
README
======
- The YASMINE (Yet Another Symbolic Modeling INteractive Engine) project started
-off in fall 2011 as a tentative and partial C++ re-implementation of the NuSMV2
-model checker. As a former member of the NuSMV2 development team (in the years
-between 2008 and 2011) I was never completely happy with a few architectural
-choices, inherited from the long history of the NuSMV model checker and/or due
-to the amount of legacy code and tools that relied on it.
-
- Overtime, however, YASMINE has significantly diverged from the original goal
-of making a NuSMV re-implementation. The input language for YASMINE is now a
-dialect of the SMV language which retains only partial compatibility with
-NuSMV's original input language. In this area, my interest is all about
-exploring ways to improve language expressiveness and usability.
-
- The project has now approached a stage in which the program is usable to
-perform basic reachability analysis and step-by-step simulation. The source
-distribution includes a few examples to demonstrate how the program can be used
-to solve planning problems.
+ The yasmv (Yet Another Symbolic Model Verifier) project started off
+in fall 2011 as a tentative and partial C++ re-implementation of the
+NuSMV2 model checker. As a former member of the NuSMV2 development
+team (in the years between 2008 and 2011) I was never completely happy
+with a few architectural choices, inherited from the long history of
+the NuSMV model checker and/or due to the amount of legacy code and
+tools that relied on it.
+
+ Overtime, however, the project has significantly diverged from the
+original goal of making a NuSMV re-implementation. The input language
+for yasmv is now a dialect of the smv language which retains only
+partial compatibility with NuSMV's original input language. In this
+area, my interest is all about exploring ways to improve language
+expressiveness and usability.
+
+ The project has now approached a stage in which the program is
+usable to perform basic reachability analysis and step-by-step
+simulation. The source distribution includes a few examples to
+demonstrate how the program can be used to solve planning problems.
BUILD
=====
- To install required dependencies on a Debian-like GNU/Linux distribution:
+ To install required dependencies on a Debian-like GNU/Linux
+ distribution:
$ sudo apt-get install autoconf libtool gcc g++ libboost-all-dev \
zlib1g-dev make minisat antlr3 libantlr3c-dev
when all the required packages are installed, launching the build
should boil down to this:
- $ autoreconf -vif (you only need to do this once)
-
$ ./setup.sh
$ make
@@ -52,11 +53,11 @@ BUILD
files you will no longer need the JRE to make the build. No JRE is
needed when running the final executable either.
- After completing the build there is one more step that needs to be
- taken before being able to actually run the program. YASMINE
- requires access to the microcode data package, which is released as
- a bz2'd tarball due to its size (currently 34 MB). Unpack the
- microcode tarball with:
+ If you didn't run the setup.sh script, when done with the build
+ there is one more step that needs to be taken in order to being able
+ to actually run the program. yasmv requires access to the microcode
+ data package, which is currently released along with the source code
+ as a bz2'd tarball. Unpack the microcode tarball with:
$ tar xfj microcode.tar.bz2 [ -C < optional-target-parent-directory > ]
@@ -65,14 +66,13 @@ BUILD
want the microcode distribution unpacked in the the same location as
the program source code:
- $ cd yasmine
$ tar xfj microcode.tar.bz2
$ export YASMV_MICROCODE=`pwd`/microcode
$ ./yasmv
- YASMINE - Yet Another Symbolic Modelling INteractive Environment
+ yasmv - Yet Another Symbolic Model Verifier
(c) 2011-2016, Marco Pensallorto < marco DOT pensallorto AT gmail DOT com >
- https://github.com/mwolf76/yasmine
+ https://github.com/mwolf76/yasmv
[Sat May 21 17:21:57 2016].459 src/main.cc:176 :: 2176 microcode fragments registered.
>>
@@ -109,6 +109,6 @@ WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
Lesser General Public License for more details.
-YASMINE is in no way related to, or endorsed by, the NuSMV2
-development board and/or FBK. YASMINE does not contain any code from
-NuSMV's code base.
+yasmv is in no way related to, or endorsed by, the NuSMV2 development
+board and/or FBK. yasmv does not contain any code from NuSMV's code
+base.
View
@@ -2,7 +2,7 @@
# Process this file with autoconf to produce a configure script.
AC_PREREQ(2.60)
-AC_INIT([gnusmv], [0.0.1], [marco.pensallorto@gmail.com])
+AC_INIT([yasmv], [0.0.5], [marco.pensallorto@gmail.com])
# where to look for install.sh and other helpers
AC_CONFIG_AUX_DIR([helpers])
@@ -43,8 +43,8 @@ BOOST_CHRONO
AC_DEFINE_UNQUOTED(PACKAGE_BUILD_DATE, "`date -u`", Build date)
# Program informations
-AC_DEFINE_UNQUOTED(PROGRAM_NAME, "Yasmine", Program Name)
-AC_DEFINE_UNQUOTED(PROGRAM_VERSION, "0.0.1", Program Version)
+AC_DEFINE_UNQUOTED(PROGRAM_NAME, "yasmv", Program Name)
+AC_DEFINE_UNQUOTED(PROGRAM_VERSION, "0.0.5", Program Version)
AC_DEFINE_UNQUOTED(PROGRAM_BUILD_DATE, "`date -u`", Program build date)
AC_DEFINE_UNQUOTED(PROGRAM_WEBSITE, "https://github.com/mwolf76", Program Website)
AC_DEFINE_UNQUOTED(PROGRAM_EMAIL, "marco.pensallorto@gmail.com", Program Email)
@@ -105,9 +105,6 @@ AC_CHECK_HEADER(malloc.h,
# antlr checks
AC_ANTLR
-# zlib check
-AX_CHECK_ZLIB
-
# readline check
AX_LIB_READLINE
@@ -130,7 +127,8 @@ AC_FUNC_VPRINTF
AC_CHECK_FUNCS([floor memmove memset pow strcasecmp strchr \
strrchr strstr strtol, random srandom getpid \
mkstemp mktemp tmpnam getenv setvbuf system popen isatty])
-AM_CPPFLAGS="$BOOST_CPPFLAGS"
+
+AM_CPPFLAGS="$BOOST_CPPFLAGS -DYASMV_MICROCODE=$datadir/$PACKAGE"
AC_SUBST(AM_CPPFLAGS)
AM_CFLAGS="-Wall -Wstrict-prototypes"
@@ -142,7 +140,7 @@ AC_SUBST(AM_CXXFLAGS)
AC_CONFIG_FILES([Makefile
src/Makefile
src/3rdparty/Makefile
- src/3rdparty/jsoncpp/Makefile
+ src/3rdparty/ezlogger/Makefile
src/cmd/Makefile
src/cmd/commands/Makefile
src/common/Makefile
@@ -163,6 +161,7 @@ AC_CONFIG_FILES([Makefile
src/model/compiler/Makefile
src/model/type_checker/Makefile
src/model/preprocessor/Makefile
+ src/opts/Makefile
src/parser/Makefile
src/parser/grammars/Makefile
src/sat/Makefile
@@ -171,6 +170,6 @@ AC_CONFIG_FILES([Makefile
src/witness/Makefile
src/witness/out/Makefile
doc/Makefile
- gnusmv.pc])
+ yasmv.pc])
AC_OUTPUT
View
@@ -0,0 +1,5 @@
+yasmv (1.0-1) UNRELEASED; urgency=medium
+
+ * Initial release. (Closes: #XXXXXX)
+
+ -- Marco Pensallorto <marco.pensallorto@gmail.com> Sat, 24 Dec 2016 09:48:12 +0100
View
@@ -0,0 +1 @@
+9
View
@@ -0,0 +1,25 @@
+Source: yasmv
+Maintainer: Marco Pensallorto <marco.pensallorto@gmail.com>
+Section: misc
+Priority: optional
+Standards-Version: 3.9.2
+Build-Depends: debhelper (>= 9)
+
+Package: yasmv
+Architecture: any
+Depends: ${shlibs:Depends}, ${misc:Depends}
+Description: Yet Another Symbolic Model Verifier
+ The yasmv project started off in fall 2011 as a tentative and partial C++
+ re-implementation of the NuSMV2 model checker. As a former member of the NuSMV2
+ development team (in the years between 2008 and 2011) I was never completely
+ happy with a few architectural choices, inherited from the long history of the
+ NuSMV model checker and/or due to the amount of legacy code and tools that
+ relied on it. Overtime, however, the project has significantly diverged from
+ the original goal of making a NuSMV re-implementation. The input language for
+ yasmv is now a dialect of the smv language which retains only partial
+ compatibility with NuSMV's original input language. In this area, my interest
+ is all about exploring ways to improve language expressiveness and usability.
+ The project has now approached a stage in which the program is usable to
+ perform basic reachability analysis and step-by-step simulation. The source
+ distribution includes a few examples to demonstrate how the program can be used
+ to solve planning problems.
View
@@ -0,0 +1,27 @@
+Format: http://www.debian.org/doc/packaging-manuals/copyright-format/1.0/
+Upstream-Name: yasmv
+Source: https://github.com/mwolf76/yasmv
+
+Files: *
+Copyright: Copyright 2010-2016 Marco Pensallorto <marco.pensallorto@gmail.com>
+License: GPL-2+
+ This program is free software; you can redistribute it
+ and/or modify it under the terms of the GNU General Public
+ License as published by the Free Software Foundation; either
+ version 2 of the License, or (at your option) any later
+ version.
+ .
+ This program is distributed in the hope that it will be
+ useful, but WITHOUT ANY WARRANTY; without even the implied
+ warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR
+ PURPOSE. See the GNU General Public License for more
+ details.
+ .
+ You should have received a copy of the GNU General Public
+ License along with this package; if not, write to the Free
+ Software Foundation, Inc., 51 Franklin St, Fifth Floor,
+ Boston, MA 02110-1301 USA
+ .
+ On Debian systems, the full text of the GNU General Public
+ License version 2 can be found in the file
+ `/usr/share/common-licenses/GPL-2'.
Oops, something went wrong.

0 comments on commit c62d1d2

Please sign in to comment.