Alloyp is an extension of Alloy4.2 supporting partial instance. You may download the executable file and document. ABZ14 experiment files

We are still working on the project, and the executable file is periodically updated. There are some recognized bugs or missed features listed below. Please contact us in case of new bug.
  1. Implementing Integer / DONE
    1. Now we are going to support the sparse ranges of Integers
  2. Support 'run {} for i'
  3. Join expression on the left hand side. (INVALID)
    1. In case of having a relation that is common between two Sigs, supporting the name-scoping would help developer.
    2. Supporting 'suppress expansion'
  4. Supporting 'moreover' keyword / DONE
  5. Implementing Appended facts or any other solution that provides the access to atoms inside the inst block from the rest of Alloy program. (DONE)
  6. Generators
  7. Extend keyword for inst block
  8. Handling the scope for Int, put 'n Int' in the inst block instead of having 'for i, 5 Int', DONE
    1. Bug. Running with multiple run-commands causes the bitwidth is overridden.(DONE?)
  9. Multiple for block and changing default number of instances in run, DONE
  10. Supporting no keyword for empty set of atoms for a variable /DONE
  11. The evaluator does not show the atoms.
  12. The parse tree does not show the inst block.
  13. A bug: In regular Alloy, an sig defined by 'in' keyword has all instances of base class; however, in the new alloy by 'extends' keyword it is met. The sample is in alloyb/translate-run/time_table/inst/bug_in_keyword.als
  14. Access to inst module atoms from different modules.
  15. Bug in type-hierarchy. DONE,
    1. Resolved by making two rules:(a. All super-sigs are abstract; b. Both super and sub-sigs cannot be in LHS of an inst block). It was implemented by employing bottom-up approach.
  16. Referring to sig names on RHS. ( e.g. r includes C0->A->B)
  17. Grouping the atoms in production. (e.g. r includes (C0+C1)->A->(B0+B1) )
  18. Add a button to the visualizer to show the solution as an inst block, similar to the buttons that now display the solution as a tree or XML
    1. Export an instance as an inst block.
  19. Facilitate error reporting for debugging.
  20. inst-block after run-command.