tabellion/instr-to-kodkod/src, branch master Verification tool for VHDL (or at least the prototype of one). https://www.segfault.tech/cgit.cgi/tabellion/atom?h=master 2017-09-27T14:02:38Z Limits the creation of atom-relations to "String". 2017-09-27T14:02:38Z Nathanael Sensfelder SpamShield0@MultiAgentSystems.org 2017-09-27T14:02:38Z urn:sha1:a3b507f3d2ce6041d29e154e11011d1f963e1a19 The need for those relations is limited to the access of their atom in the formula. As, with the exception of String elements, the formula cannot directly reference an atom, only String atoms require their own relation. Going even further, only the String element referenced in the formula need their own relation. Got some property dependencies to work. 2017-09-21T13:26:01Z Nathanael Sensfelder SpamShield0@MultiAgentSystems.org 2017-09-21T13:26:01Z urn:sha1:0fc661ebabdf55b8e0d26c4f85f0547c106b6549 Solves the missing solutions bug. Starts PropDeps. 2017-09-20T15:19:42Z Nathanael Sensfelder SpamShield0@MultiAgentSystems.org 2017-09-20T15:19:42Z urn:sha1:bc3e8933e1005e93e4a97b9a207cb40db454a2a8 Strings are all in lowercase. 2017-09-19T15:15:27Z Nathanael Sensfelder SpamShield0@MultiAgentSystems.org 2017-09-19T15:15:27Z urn:sha1:9d6c35b2e847e6e4864e550574ab08f2c9d20ee6 Still doesn't fix CNE_01200's valid.vhd:19 not being detected. The instr model seems correct, though. Fixes anonymous strings, adds CNE_01100 test. 2017-09-19T14:12:54Z Nathanael Sensfelder SpamShield0@MultiAgentSystems.org 2017-09-19T14:12:54Z urn:sha1:0b35af5ee0e660c810e22a09738ff1960745db23 Removes the extra set of " that messed with regex. 2017-09-19T14:08:48Z Nathanael Sensfelder SpamShield0@MultiAgentSystems.org 2017-09-19T14:08:48Z urn:sha1:8a15d57b056cf84aa9b2ae0234bf5bc432b414c3 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 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 Adds a verbosity parameter. 2017-07-31T12:28:50Z Nathanael Sensfelder SpamShield0@MultiAgentSystems.org 2017-07-31T12:28:50Z urn:sha1:05fbf26dbb1b1f19e3ef76a0d0789806fa7be12c