summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2017-09-18Merge branch 'instance-calculator'Nathanael Sensfelder
2017-09-04Fixes jar not downloading.Nathanael Sensfelder
2017-08-30Reduces the scalability issue.Nathanael Sensfelder
It seems to take very long to find solutions for simple_flip_flop_instance, but at least it no longer gives up right away.
2017-08-30Gets stuck due to scaling issues.Nathanael Sensfelder
2017-08-28Small changes? Forgot to commit.Nathanael Sensfelder
2017-08-16Fixes Makefiles so they can run parallel jobs.Nathanael Sensfelder
2017-08-15Partial attr. support, build/run targets, literalsNathanael Sensfelder
2017-08-15Adds support for comments in properties.Nathanael Sensfelder
2017-08-15Adds 'eq' and 'iff' to the language.Nathanael Sensfelder
2017-08-04For some reason, CNE_01700 no longer works.improved_makefilesNathanael Sensfelder
2017-08-03Fixes issues in properties, Makefiles.Nathanael Sensfelder
2017-08-03Other than the pretty-printer, it seems done.Nathanael Sensfelder
2017-08-03The Makefile of instr-to-kodkod's parser is done.Nathanael Sensfelder
2017-08-03Improving clarity through better Makefiles.Nathanael Sensfelder
2017-08-01Starting a pretty-printer for the solutions.Nathanael Sensfelder
2017-08-01Fixes is_accessed_by. CNE_01700 is not working.Nathanael Sensfelder
The BCE has been updated to include a group of items that should be tagged by the CNE_01700 rule. However, it's not happening. I don't see anything wrong with the way the CNE_01700 rule is written and a quick overview of the generated model would lead me to conclude that it indeed should tag something. Likely there are still issues with the way properties are turned into Kodkod formulas.
2017-08-01Fixes regex predicate + optimizes CNE_01700.Nathanael Sensfelder
The combination of those two changes makes the solving much faster, but since BCE does not have anything that would be matched, it may also simply be incorrect.
2017-07-31Fixes typo with functions, errors in grammar.Nathanael Sensfelder
Looking for the groups matching CNE_01700 appears to take a really long time. The formula is quite complex, yet unlikely to be one of the most complex ones, so we'll have to see what can be done.
2017-07-31First shot at the handling of regular expressions.Nathanael Sensfelder
2017-07-31Adds a verbosity parameter.Nathanael Sensfelder
2017-07-31Finer imports.Nathanael Sensfelder
2017-07-31Improves solution displaying.Nathanael Sensfelder
2017-07-31Tagged variables are now the only skolemized vars.skol_only_the_solutionNathanael Sensfelder
2017-07-28Removes repetitions, prepares for skol. of sol.Nathanael Sensfelder
2017-07-27Fixes multiple issues with depths.Nathanael Sensfelder
2017-07-27First shot at depths operators.Nathanael Sensfelder
2017-07-26(Woops) Adds anonymous strings support.Nathanael Sensfelder
2017-07-26First shot at (logic, not VHDL) functions.Nathanael Sensfelder
2017-07-25Gets the strings seemingly working.Nathanael Sensfelder
2017-07-25It seems to work.Nathanael Sensfelder
2017-07-25Fixes issues with "_". things seem to work now.Nathanael Sensfelder
2017-07-25Improves error reports for the property.Nathanael Sensfelder
2017-07-24Lets users use projections in predicates.Nathanael Sensfelder
2017-07-24Fixes connect_to/node_connect, configs Makefiles.Nathanael Sensfelder
2017-07-20Removes TODO from the grammar.Nathanael Sensfelder
2017-07-19Formula.and(Formula...) != a.and(Formula...)Nathanael Sensfelder
Having both a static and a non-static function share a name does not seem like a sane decision.
2017-07-19This one seem to work -> bad CTL?Nathanael Sensfelder
2017-07-19forgot to use cfg-to-path. Still broken though.Nathanael Sensfelder
2017-07-19The formula seems correct, which is worrisome.Nathanael Sensfelder
2017-07-19Signals being used instead of wfm + rec targetsNathanael Sensfelder
Those Python scripts may have to be cleaned up at some point...
2017-07-19No longer add function and literals as waveforms.Nathanael Sensfelder
2017-07-19More small mistakes removed. It seems to work now.Nathanael Sensfelder
2017-07-19Adds messages to follow the framework's flow.Nathanael Sensfelder
2017-07-19Fixes stupid mistakes.Nathanael Sensfelder
2017-07-19First shot at the framework (it does compile).Nathanael Sensfelder
2017-07-18Adds missing predicate from g4 to instr scriptsNathanael Sensfelder
2017-07-18It compiles... Ship it!Nathanael Sensfelder
2017-07-18Starting to link parser with the program.Nathanael Sensfelder
But apparently I messed up some kodkod logic.
2017-07-18Unused predicates & types -> not in kodkod.Nathanael Sensfelder
2017-07-18Antlr now creates the associated Java files.Nathanael Sensfelder
Next step is to get those to compile.