Re:Learn TLA+ (2018)
by sterlind on Sunday February 23, 2020 @02:33AM
(#22395631)
I've actually built something like this for TLA+ and C#, which I call Kayfabe. I'll hopefully present it this October at the next TLA+ conference.
High-level, there are two modes:
1. Checking execution traces from running code against the model (see notpron's work for this idea)
2. Outputting every state visited by the model checker in a finite instantiation, then computing paths to step the real C# through so it'll visit every state or transition at least once. This is very, extremely computationally expensive, but I'm running real code in prod that I've tested this way.
Hopefully I can get my algorithms to be efficient and if so I'll try to open-source my efforts.
High-level, there are two modes:
1. Checking execution traces from running code against the model (see notpron's work for this idea)
2. Outputting every state visited by the model checker in a finite instantiation, then computing paths to step the real C# through so it'll visit every state or transition at least once. This is very, extremely computationally expensive, but I'm running real code in prod that I've tested this way.
Hopefully I can get my algorithms to be efficient and if so I'll try to open-source my efforts.