Artur Meski
|
2b7d5e77dd
|
enc_max
|
2017-08-15 21:41:41 +01:00 |
|
Artur Meski
|
15cbf62e82
|
Max encoding, WIP
|
2017-08-14 21:31:43 +01:00 |
|
Artur Meski
|
9ca4d3954f
|
Initial encoding of reactions
|
2017-08-13 20:11:25 +01:00 |
|
Artur Meski
|
dd4ea5d939
|
cleanup
|
2017-08-13 16:02:22 +01:00 |
|
Artur Meski
|
c83779c9d5
|
Declaration of the intermediate product variables for the reactions and entities that are actually used as products
|
2017-08-13 15:51:20 +01:00 |
|
Artur Meski
|
27c86497e4
|
RSC with Param; RSCA for Param, SMTChecker for Param
|
2017-08-13 13:48:42 +01:00 |
|
Artur Meski
|
e1db24c8a9
|
SMTChecker for RSC, for the new parametic-compatible encoding
|
2017-08-13 12:26:43 +01:00 |
|
Artur Meski
|
55ff688fd0
|
add RSC with param for the new encoding suitable for parametric verification
|
2017-08-09 20:57:52 +01:00 |
|
Artur Meski
|
fec235a6a1
|
Version number
|
2017-07-21 14:33:42 +01:00 |
|
Artur Meski
|
f28edea6ac
|
added constraint for ctx aut states in state equivallence encoding
|
2017-04-08 18:15:16 +02:00 |
|
Artur Meski
|
7746c364f1
|
gen_dat script
|
2017-04-04 22:49:05 +02:00 |
|
Artur Meski
|
9c9084e4e2
|
simple rsLTL example for paper
|
2017-04-04 22:48:33 +02:00 |
|
Artur Meski
|
cabe9fc1b8
|
operators
|
2017-04-04 22:48:11 +02:00 |
|
Artur Meski
|
b22fcd8015
|
cleanup; flush_cache
|
2017-03-19 20:50:01 +01:00 |
|
Artur Meski
|
a51f4e5ed2
|
new results
|
2017-03-19 20:28:02 +01:00 |
|
Artur Meski
|
5a34d4028b
|
Cache. Massive improvement
|
2017-03-19 15:58:44 +01:00 |
|
Artur Meski
|
9cf5477169
|
new results for f2
|
2017-03-19 11:26:33 +01:00 |
|
Artur Meski
|
2a5750976a
|
new experimental results for f4, f5
|
2017-03-18 18:56:25 +01:00 |
|
Artur Meski
|
565d1c070d
|
Aesthetics, printing of rsLTL formulae
|
2017-03-18 18:40:33 +01:00 |
|
Artur Meski
|
15500b7e38
|
New formula, 5
|
2017-03-18 18:39:52 +01:00 |
|
Artur Meski
|
80f2caea53
|
experimental results
|
2017-03-17 09:32:09 +01:00 |
|
Artur Meski
|
ab5550d3fd
|
benchmarks for SC
|
2017-03-16 20:57:42 +01:00 |
|
Artur Meski
|
59cd3af3e1
|
Formulae for Scalable Chain; some fixes and improvements
|
2017-03-15 23:30:29 +01:00 |
|
Artur Meski
|
56d4d8fde8
|
Sanity checks for bags.
|
2017-03-15 22:33:14 +01:00 |
|
Artur Meski
|
9ed2104757
|
Changed back to the old solver (BMC never finished)
|
2017-03-13 22:31:08 +01:00 |
|
Artur Meski
|
b0bfa4a13f
|
Updated version string
|
2017-03-13 22:29:55 +01:00 |
|
Artur Meski
|
36f571c0d1
|
Switched to QF_FD (smt checker for rsc)
|
2017-03-13 22:06:33 +01:00 |
|
Artur Meski
|
7f6ea619b2
|
reset & initialise methods for SMT Checker; fixed some typos for rsLTL
|
2017-03-12 23:33:04 +01:00 |
|
Artur Meski
|
05557440a0
|
preparing for experiments, HSR -- reachability testing via rsLTL; some cleanup
|
2017-03-12 15:29:28 +01:00 |
|
Artur Meski
|
5934c6381d
|
Bugfix: bad variable name for the implementation of the Globally operator
|
2017-03-12 14:38:18 +01:00 |
|
Artur Meski
|
20f66b5556
|
Makefile
|
2017-03-12 12:51:49 +01:00 |
|
Artur Meski
|
20464ac6dd
|
bugfix for F and G encodings -- missing element for i=k
|
2017-03-12 12:50:09 +01:00 |
|
Artur Meski
|
fab7880ccf
|
working on the new encoding
|
2017-03-11 19:57:42 +01:00 |
|
Artur Meski
|
97ff4baf35
|
working on the new encoding; backup commit
|
2017-03-09 23:06:44 +01:00 |
|
Artur Meski
|
f70cc0034b
|
implementation for encoding or rsLTL (without loop)
|
2017-03-05 17:41:26 +01:00 |
|
Artur Meski
|
827568e174
|
working on the encoding for rsLTL, testing functionality
|
2017-03-05 12:58:24 +01:00 |
|
Artur Meski
|
12fee678f6
|
encoder
|
2017-03-05 12:33:07 +01:00 |
|
Artur Meski
|
a91b7c732e
|
working on the encoder
|
2017-03-05 10:47:35 +01:00 |
|
Artur Meski
|
9fb4e4a343
|
encoder
|
2017-03-03 20:08:06 +01:00 |
|
Artur Meski
|
ed1d9433a6
|
added logics module
|
2017-03-02 21:00:20 +01:00 |
|
Artur Meski
|
821df2e152
|
cleanup
|
2017-03-02 20:59:34 +01:00 |
|
Artur Meski
|
2abf76ae72
|
logics module
|
2017-03-02 20:59:07 +01:00 |
|
Artur Meski
|
68c824e2f1
|
Parameters for rsLTL
|
2017-03-01 21:08:41 +01:00 |
|
Artur Meski
|
bae7611606
|
Renaming FormulaLTL -> Formula_rsLTL
|
2017-02-26 22:27:49 +01:00 |
|
Artur Meski
|
d065dbac83
|
Renaming FormulaLTL -> Formula_rsLTL
|
2017-02-26 22:27:29 +01:00 |
|
Artur Meski
|
4e7d640e2f
|
Bag descriptions; oper. overloading for FormLTL and BagDescription
|
2017-02-26 22:23:06 +01:00 |
|
Artur Meski
|
ac389b238b
|
working on smt encoding for NA
|
2017-01-01 18:23:02 +01:00 |
|
Artur Meski
|
1594659509
|
getters for the used actions, automata supporting actions, transitions for actions, etc.
|
2017-01-01 00:34:27 +01:00 |
|
Artur Meski
|
ebee3aa03e
|
working on RSNA
|
2016-12-29 20:21:56 +01:00 |
|
Artur Meski
|
ba8cb798e4
|
clean and cleanall
|
2016-12-29 20:15:11 +01:00 |
|