Yet again the solution to figuring out a gnarly microcontroller scheduling problem is to write a custom emulator to get rid of "actual time".
Conversation
This always seems like a lot of work at the onset, but dramatically shifts the effort from spending time in debugging to spending time in modeling.
1
2
Combined the deterministic discrete event simulator with a QuickCheck style stimulus generator. A "property" is a an interpreter for a generated test program: it interacts with the emulated network from clean reset, and produces a false result if any internal assertion fails.
1
Doing it at the integration test level is an intermediate approach. I currently can't properly specify corner cases of all state machines, otherwise this would be possible:
1
You can't replace testing with types, but can you replace types with testing?
I mean obviously lack of counterexample is not proof, but is it good enough when you're stuck with a lot of code in language like Lua? I mean Hughes is talking about Erlang after all...
Replying to
Added shrinking to my minimal Lua QC implementation. I found a neat way to encode the generators and shrinkers, instantiating from HOAS that describes the types. Will publish when I have used it for uc_tools unit tests. For now some bits are in lua/lib/qctools.lua
1
This was an interesting experience. I didn't know what I was doing for a while but kept coming back to "focus on composition, and compose with functions" and eventually, out falls a very succinct encoding. Probably nothing original just stoked that it kind of wrote itself.