Is there a language/framework can describe a model and generate checking rules? | Hacker News Reader

Is there a language/framework can describe a model and generate checking rules?

9 pointslinq9367 comments

We have a fairly complex embedded system. I have been writing a Python script to analyze its register dump and narrow down the problem areas. But it is quite tedious writing such script, because I have to write a lot of code such as, the 1st bit of register 1 must equal to the 3rd bit of register 2; another example, register 3 plus register 4 must be no more than register 5 when register 6 is greater than 100.

I am thinking to write a DSL, Domain Specific Language, to describe the system specification and that DSL will generate Python code which does the checking.

Before I do this, is there a ready tool/framework/technology/language I can leverage?

Someone mentioned TLA+, my first glimpse tells me it is not for my need. Like to hear your suggestions.

Thanks.

View on HN

As others have said, using a combinatorial solver like Z3 (SMT solver) or MiniZinc (which is a modelling language and can interface to different types of solvers, including several constraint programming and mixed integer programming solvers, can be driven via minizicn-python) is probably the way to go. CPMpy is a new Python modelling framework that might also be of interest that interfaces to different solvers

If you have a lot of constraints that are on the bit representation, then it is more likely that an SMT solver is a better solution. If on the other hand more of your constraints are arithmetic and perhaps some structural constraints, then it might be interesting to look into other types of solvers. It all depends on the specifics of your problem instances.

There are a couple of Coursera courses for modelling with MiniZinc that are quite nice (https://www.coursera.org/learn/basic-modeling is the first one) that are useful if you want to learn more about how to think when doing combinatorial modelling. These are usefule even if you end up using some other tool or technology, as the mindset is similar.

Maybe you could use an SMT solver like Z3. It lets you write formulas constraining the values of bit arrays and numeric variables and then produce counterexamples if the constraints are inconsistent.

Yeah, Z3 is the first thing I'd try here, then maybe MiniZinc if that didn't pan out.

If the logic you are checking is tedious then using a different tool won’t necessarily help you. You still have to explain all the tedious details to that tool. Perhaps making your own abstractions in Python might work better. If you have a lot of “this bit needs to match that bit in this register” then add a function that takes just the bit/register numbers and automatically does the rest. Then you have in a sense created your own DSL within Python. Learning a new complex tool like Z3 will most likely take longer than just doing it in Python. However it might be fun to learn Z3 of course.

As understood it, finding a solution that satisfies all the constraints is not trivial, and for that external libraries are the right kind of tool.

It seems you want helper functions to read that dump and then a bunch of unit tests? Then any Python testing framework would help.

But I don't know what you mean by writing rules automatically. How would such framework figure out your business rules?

Use a language (DSL or general) that can provide a rules engine. Prolog could be suitable for this.

Reply on news.ycombinator.com