← Back to context Comment by vatsachak 2 months ago Gotta love TLA+I wonder if anyone has worked on porting it to Lean and making tactics for it 2 comments vatsachak Reply uptodatenews 2 months ago You run into Rices theorem if you try to apply it too heavily.I made https://github.com/RCSnyder/tlaplus-process-studiohttps://tlaplus-process-studio.com/For local only high level modelling. Its not a full tie into the actual model checker, but its meant to serve as a first step into system modelling for state machine modelling for beginners another_twist 2 months ago i am not sure if a lean port is important. TLA+ could do with a bit more TLC (pun intended) with regards its devEx.Also congratulations to the author, I'll try and reproduce this over the weekend.
uptodatenews 2 months ago You run into Rices theorem if you try to apply it too heavily.I made https://github.com/RCSnyder/tlaplus-process-studiohttps://tlaplus-process-studio.com/For local only high level modelling. Its not a full tie into the actual model checker, but its meant to serve as a first step into system modelling for state machine modelling for beginners
another_twist 2 months ago i am not sure if a lean port is important. TLA+ could do with a bit more TLC (pun intended) with regards its devEx.Also congratulations to the author, I'll try and reproduce this over the weekend.
You run into Rices theorem if you try to apply it too heavily.
I made https://github.com/RCSnyder/tlaplus-process-studio
https://tlaplus-process-studio.com/
For local only high level modelling. Its not a full tie into the actual model checker, but its meant to serve as a first step into system modelling for state machine modelling for beginners
i am not sure if a lean port is important. TLA+ could do with a bit more TLC (pun intended) with regards its devEx.
Also congratulations to the author, I'll try and reproduce this over the weekend.