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.
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...
1
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.