Blog: 11/14/22

Ok, TLA Toolbox is one of the obstacles. ProbablyJupiter notbook will work better as an IDE. The problem is that README doesn't specify how to pass all parameters to TLC model checker and refers to the book that is not available... Wrappers for command line Looks like TLC command line tool and passing argument is some special art. Ok, models are parameterized by *.cfg file. The file is generated by toolbox or pcal from the wrappers list. The list of options

INVARIANT 

INVARIANTS 

PROPERTY 

PROPERTIES 

CONSTANT 

CONSTANTS 

CONSTRAINT 

CONSTRAINTS 

ACTION_CONSTRAINT 

ACTION_CONSTRAINTS 

INIT 

NEXT 

VIEW 

SYMMETRY 

TYPE 

TYPE_CONSTRAINT

So in jupiter-notebook I can specify CONSTANT like

CONSTANT S <- SSizeRange

Blog: 11/12/22

Long story short - formal methods and robots. I have 2 things Bitty Robot and one another related to work. What I want to reach with formal methods?.. Good question if I only know what formal methods are capable for. Let start with survay

Luckcuck, M., Farrell, M., Dennis, L., Dixon, C., & Fisher, M. (2018). Formal Specification and Verification of Autonomous Robotic Systems: A Survey. https://doi.org/10.1145/3342355