tabellion/instr-to-kodkod, branch improved_makefiles Verification tool for VHDL (or at least the prototype of one). https://www.segfault.tech/cgit.cgi/tabellion/atom?h=improved_makefiles 2017-08-04T10:47:30Z For some reason, CNE_01700 no longer works. 2017-08-04T10:47:30Z Nathanael Sensfelder SpamShield0@MultiAgentSystems.org 2017-08-04T10:47:30Z urn:sha1:d18ca72caf2004c7725b3de670c7397c5bf85eb4 Fixes issues in properties, Makefiles. 2017-08-03T15:17:38Z Nathanael Sensfelder SpamShield0@MultiAgentSystems.org 2017-08-03T15:17:38Z urn:sha1:43cb556708d727376724eac0e67207c28d1761bf Other than the pretty-printer, it seems done. 2017-08-03T14:57:20Z Nathanael Sensfelder SpamShield0@MultiAgentSystems.org 2017-08-03T14:57:20Z urn:sha1:71f3a1bb063087e51f2b2e2ef940e773e2e084d1 The Makefile of instr-to-kodkod's parser is done. 2017-08-03T14:02:19Z Nathanael Sensfelder SpamShield0@MultiAgentSystems.org 2017-08-03T14:02:19Z urn:sha1:b16812434d54a9d7480564cbf4f299168ca6a1a1 Improving clarity through better Makefiles. 2017-08-03T13:28:17Z Nathanael Sensfelder SpamShield0@MultiAgentSystems.org 2017-08-03T13:28:17Z urn:sha1:90bb7e959496c3a12bebe055f6344b9f06f22809 Starting a pretty-printer for the solutions. 2017-08-01T14:26:48Z Nathanael Sensfelder SpamShield0@MultiAgentSystems.org 2017-08-01T14:26:48Z urn:sha1:69d904f3b2de5b914bc329af1729584f10644bf2 Fixes is_accessed_by. CNE_01700 is not working. 2017-08-01T09:10:01Z Nathanael Sensfelder SpamShield0@MultiAgentSystems.org 2017-08-01T09:10:01Z urn:sha1:4637db06583bc250b96e6145fc7bac9e16c730df 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. Fixes regex predicate + optimizes CNE_01700. 2017-08-01T08:04:25Z Nathanael Sensfelder SpamShield0@MultiAgentSystems.org 2017-08-01T08:04:25Z urn:sha1:798dea30c7832f8c6364d1734423c6a6fda1ce57 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. Fixes typo with functions, errors in grammar. 2017-07-31T15:04:51Z Nathanael Sensfelder SpamShield0@MultiAgentSystems.org 2017-07-31T15:04:51Z urn:sha1:bc8e275546e2e6fe6bcf19ce42c0fab07eecdf4c 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. First shot at the handling of regular expressions. 2017-07-31T13:05:30Z Nathanael Sensfelder SpamShield0@MultiAgentSystems.org 2017-07-31T13:05:30Z urn:sha1:067f596822b80b2786ce2bb895a593d479516cad