Which new features would you like to see in Clafer?

by Michał Antkiewicz

We are thinking of implementing a few new features for Clafer. We opened a poll on the right, above the "Blog Archive". Please vote.

Here's a brief explanation of the features:

• redefinition
  Allows for defining a clafer with the same name as the inherited one and restricting it's group cardinality, clafer cardinality, reference type, and bag to set. This is particularly useful for Example-Driven Modeling and specialization in architecture (e.g., Autosar uses it).

• module system
  Allows for splitting a large model into smaller ones and also reusing common models. We are currently working on a simplest possible module system that will compile multiple files inside a single namespace.

• temporal constraints
  Allow for specifying how model instances can evolve over time. In that view, the current Clafer constraints become simply global invariants. Using temporal constraints one can specify valid sequences of model instances. We're currenlty working on adding LTL constraints to Clafer and some more convenient syntactic sugar for behavior specification patterns and guarded and unguarded transitions.

• real numbers
  Allow for reasoning on Real number arithmetic. We're planning on providing support in the ClaferSMT backend.

• string constraints
  Allow for constraining the valid values of strings (using equality, prefix, postfix, maybe regexp) and operations on strings such as concatenation.

• inverse relation
  Allows for conveniently specifying that two references are mutually inverse.

• transitive closure
  Allows for specifying constraints over paths in recursive structures, such as, lists, trees and graphs.

We would like to have them all but we must put some priorities. Please choose the ones most important for you.

Also, please post comments with other feature suggestions not on this list.