1. 22
  1.  

  2. 10

    The main addition in Alloy 6 is time syntax, so it should be more suitable for modeling concurrency. This potentially makes it a simpler alternative to using a more heavyweight speclang like TLA+. I haven’t used it myself and probably won’t be able to get to it for a while, but I’m hoping to have alloydocs updated by the end of the year or so.

    1. 1

      Wow, thanks for the highlight and for your effort into alloydocs. What a wonderful release!

    2. 1

      It’s a bit misleading since the download page still mentions that the latest available version is Alloy 5, but the link to the latest build actually targets the version 6.0.0. Ideally this should be updated. In anyway I can’t wait to give it a try, the last time I attempted to use Alloy to model something serious I struggled a lot to deal with time. These new additions look great!

      1. 2

        Hi, I’m one of the authors of this addition to Alloy. Indeed, the site ins’t fully up-to-date yet but it should be soon. This version of Alloy is a rebranding/reshaping of an open-source extension code-named Electrum, that we’ve been developing and using for several years. I think the summary by Hillel is right on the nose. Feel free to ask any question.