Cool. That’s definitely useful. I keep going back and forth on how to structure assertions. Labeled facts gives them a bit of a boost unless signature restrictions can also be labeled in which case back to mostly even points.
I think the current “best practice” is to prefer global facts over signature facts because
no need to use this or @relation
One less bit of syntax and logic to think about
Easier to turn into predicates that you can turn on and off at will
That said, it seems that the analyzer seems to be able to SAT signature facts faster than global facts. Normally not a big improvement but it’s sometimes the different between being on a good solver path and a bad one.
I wrote a quick summary of the differences here. tl;dr is they’re both extremely useful arms while they have their specialities, they’re both effective outside that too.
The main difference comes down to the logic and workflows. The logic in Alloy is first order relational logic and in TLA+ it is a modal logic of time and actions. Both are very expressive so almost all systems can be modeled in either one but some problems are more naturally expressed in one or the other depending on which aspects of the system being modeled you want to emphasize.
I personally like Alloy better but I don’t think it’s better or worse than TLA+ and you can’t go wrong with learning either one. I seem to think better with relational structures than temporal properties so Alloy fits my thinking better in general.
I like how clean your model is and I love how you’re getting the Alloy word out.
One undocumented QoL improvement: you can label facts with strings. So if you want you can write
Cool. That’s definitely useful. I keep going back and forth on how to structure assertions. Labeled facts gives them a bit of a boost unless signature restrictions can also be labeled in which case back to mostly even points.
I think the current “best practice” is to prefer global facts over signature facts because
thisor@relationThat said, it seems that the analyzer seems to be able to SAT signature facts faster than global facts. Normally not a big improvement but it’s sometimes the different between being on a good solver path and a bad one.
Learning TLA is on my to-do list, but Alloy syntax looks much nicer. I assume their focus is different though.
I wrote a quick summary of the differences here. tl;dr is they’re both extremely useful arms while they have their specialities, they’re both effective outside that too.
The main difference comes down to the logic and workflows. The logic in Alloy is first order relational logic and in TLA+ it is a modal logic of time and actions. Both are very expressive so almost all systems can be modeled in either one but some problems are more naturally expressed in one or the other depending on which aspects of the system being modeled you want to emphasize.
I personally like Alloy better but I don’t think it’s better or worse than TLA+ and you can’t go wrong with learning either one. I seem to think better with relational structures than temporal properties so Alloy fits my thinking better in general.