issues
search
roberthsheng
/
STL-SMTLIB
STL to SMT-LIB compiler based on definitions from "A Truly Robust Signal Temporal Logic: Monitoring Safety Properties of Interacting Cyber-Physical Systems under Uncertain Observation"
https://publications.cispa.saarland/3654/1/algorithms-15-00126-v2.pdf
0
stars
0
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
Make it easier to pass in values/csvs/formulae
#26
roberthsheng
opened
1 year ago
0
Should simplification be done while parsing?
#25
roberthsheng
opened
1 year ago
0
laugh out loud!
#24
roberthsheng
closed
1 year ago
1
Section 5, step 6 of paper is incorrect.
#23
roberthsheng
closed
1 year ago
2
Can't just 'smt_list.append(formula)'
#22
roberthsheng
closed
1 year ago
0
Design Tseitin to prevent nested Tseitin
#21
roberthsheng
closed
1 year ago
1
Simplification of transformed formulas
#20
roberthsheng
opened
1 year ago
0
Simplification of nested UNTILs
#19
roberthsheng
closed
1 year ago
1
unsatisfiable statements return sat by flipping aux vars
#18
roberthsheng
closed
1 year ago
0
Issue with checking not(phi)
#17
roberthsheng
closed
1 year ago
1
Fix the use of True and False in UNTIL statements
#16
roberthsheng
opened
1 year ago
0
Nesting UNTIL Statements
#15
roberthsheng
closed
1 year ago
0
extract only useful times (times in UNTIL statement) from {csv? clauses? other?}
#14
roberthsheng
closed
1 year ago
1
create test csv for value insertion
#13
roberthsheng
closed
1 year ago
0
Duration to prevent impossible measurements
#12
roberthsheng
closed
1 year ago
1
Identify how to pass in measured values
#11
roberthsheng
closed
1 year ago
0
tseitin transformation on mathematical statements should be evaluated before solved
#10
roberthsheng
closed
1 year ago
1
plug (a2 + b2) back into p9
#9
roberthsheng
closed
1 year ago
3
Develop testing for updated Tseitin
#8
roberthsheng
closed
1 year ago
0
Temporal properties for phi
#7
roberthsheng
closed
1 year ago
0
Develop trajectory and duration logic
#6
roberthsheng
closed
1 year ago
1
Implement Tseitin Transformation to prevent exponential blowup
#5
roberthsheng
closed
1 year ago
0
Alter [t, t'] to token type LOWER, UPPER for only natural numbers
#4
roberthsheng
closed
1 year ago
0
Move bounds to after U
#3
roberthsheng
closed
1 year ago
0
Add support for modalities F[t, t] phi, G[t, t] phi
#2
roberthsheng
opened
1 year ago
0
Add support for implies (=>) Boolean connective
#1
roberthsheng
closed
1 year ago
0