Tuesday, September 12, 2023

Clafer compiler, IG, and wiki 0.5.1 released

 by Michał Antkiewicz, Sep 12, 2023

This is mostly a maintenance release bringing compatibility with the current Haskell compiler, tools, and dependencies.

Clafer compiler, release pull request (0.5.1).
  • compatibility with GHC 9.4.6.
Clafer instance generator, release pull request (0.5.1).
  • uses clafer-0.5.1
  • compatibility with GHC 9.4.6.
  • respect --json when using --all
Clafer wiki, release pull request (0.5.1).
  • uses clafer-0.5.1
  • compatibility with GHC 9.4.6.
  • gitit-0.15.1.1
The Clafer model wiki"Traffic Lights" Domain Model Example wiki, and Train Station Layout Case Study wiki are currently running clafer 0.5.1 and claferwiki-0.5.1.

Sunday, January 6, 2019

New paper "Clafer: Lightweight Modeling of Structure, Behaviour, and Variability"

by Michał Antkiewicz, Jan 6, 2019

Our new paper "Clafer: Lightweight Modeling of Structure, Behaviour, and Variability" has been published in the journal The Art, Science, and Engineering of Programming.

Abstract

Embedded software is growing fast in size and complexity, leading to intimate mixture of complex architectures and complex control. Consequently, software specification requires modeling both structures and behaviour of systems. Unfortunately, existing languages do not integrate these aspects well, usually prioritizing one of them. It is common to develop a separate language for each of these facets

In this paper, we contribute Clafer: a small language that attempts to tackle this challenge. It combines rich structural modeling with state of the art behavioural formalisms. We are not aware of any other modeling language that seamlessly combines these facets common to system and software modeling.

We show how Clafer, in a single unified syntax and semantics, allows capturing feature models (variability), component models, discrete control models (automata) and variability encompassing all these aspects. The language is built on top of first order logic with quantifiers over basic entities (for modeling structures) combined with linear temporal logic (for modeling behaviour). On top of this semantic foundation we build a simple but expressive syntax, enriched with carefully selected syntactic expansions that cover hierarchical modeling, associations, automata, scenarios, and Dwyer’s property patterns.

We evaluate Clafer using a power window case study, and comparing it against other notations that substantially overlap with its scope (SysML, AADL, Temporal OCL and Live Sequence Charts), discussing benefits and perils of using a single notation for the purpose.


NOTE: Behavioral Clafer does not currently have reasoning capabilities. The compiler implements the syntax of the language and it can desugar the syntactic sugar and produce HTML rendering. For the instance generation and multi-objective optimization capabilities, it's best to use the static Clafer 0.4.5, which works best with all instance generators and web tools.

Tuesday, September 18, 2018

"Clafer: unifying class and feature modeling" available publicly on Springer's SharedIt

by Michał Antkiewicz, Sep 18, 2018

Our paper  "Clafer: unifying class and feature modeling" can now be accessed freely via Springer's SharedIt initiative using the following link:

https://rdcu.be/6eU3

Enjoy!

Tuesday, May 8, 2018

Behavioral Model Set

by Michał Antkiewicz, May 08, 2018

Clafer Model Wiki contains a few example models showcasing behavioral Clafer.
  1. TrafficLight. A simple state machine model for traffic light transitions.
  2. PowerWindow. Our main case study from the behavioral Clafer paper.
  3. WebSocketProtocol.
  4. TLS Handshake.

Thursday, February 1, 2018

Clafer Compiler 0.5.0 Released

by Michał Antkiewicz, Jan 31, 2018

This release contains only the Clafer compiler 0.5.0, which now includes support for modeling behavior. The release does not include reasoning capability; for structural modeling and reasoning keep using the previous release 0.4.5.

Binary builds are available from Clafer Tools - Binary Distributions.

Clafer compiler, release pull request (0.5.0).
  • support for behavioral modeling,
  • ability to compile, desugar, and render to HTML behavioral models,
  • test suite of behavioral models,
  • experimental Alloy code generator,
  • compatibility with GHC 8.2.2.
The Clafer model wiki is currently running Clafer 0.5.0.

Friday, September 22, 2017

Best paper award for SoSyM 2017

by Michał Antkiewicz, Sep 22, 2017

Our paper "Synthesis and exploration of multi-level, multi-perspective architectures of automotive embedded systems" published in the Software and Systems Modeling journal has won one of the six best paper awards for year 2017.

Congratulations to our students Jordan Ross, Jimmy Liang, and Alexandr Murashkin!

The work presented in the paper was Jordan's master's thesis work based on previous master's thesis work by Alexandr. Jimmy made it all possible by contributing chocosolver, the scalable Clafer backend.

Monday, September 18, 2017

Clafer Tutorial at CBSOFT'17

by Michał Antkiewicz, Sep 18, 2017

Today, prof. Andrzej Wąsowski (IT University of Copenhagen) delivered a 3.5h tutorial entitled "Domain Modeling and Variability Modeling in Clafer" at CBSOFT'17, Fortaleza, Brazil.

The tutorial introduced the Clafer language and the participants used the online Clafer tools to write and analyze their models.

Abstract

Variability Modeling is a key activity in implementing Software Product Lines and highly configurable systems. Clafer is a small language for domain modeling with excellent support for variability modeling.  In this tutorial, we will introduce the basics of variability modeling and the basics of the  Clafer language.  Most of the tutorial will be interactive. The participants will use online Clafer tools to create basic models and analyze them, including consistency checking of models, and finding optimal configurations. Time permitting, we will discuss extensions of Clafer beyond structural domain modeling.

Tuesday, March 21, 2017

Behavioral Clafer

by Michał Antkiewicz, Mar 21, 2017

Behavioral Clafer was finally merged into develop, which means it will be part of the next release: 0.5.0.

That is a huge step for Clafer because it adds capability of modeling how the structures evolve over time. In that context, all possible instances of a static Clafer model can be considered as all possible snapshots (statespace) of a dynamic model. Also, the constraints in a static model can be considered as global invariants in a dynamic model.

The Clafer Model Wiki and the Clafer Tools (Visualizer, Configurator, and IDE) have been updated to use the 0.5.0 version; however, there is currently no reasoning support for the behavioral constructs. The models can only be compiled, desugared, and rendered to HTML.

We added two example models to showcase the behavioural modeling style:
  • Simplified Web Socket Protocol - a simple model showcasing state modeling, trace specification, and the intended traces.
  • Power Window - a complex model showcasing modeling structure and behaviour with variability: feature modeling, component modeling, statemachine modeling, variability in behaviour using alphabet variability, inheritance, and strategy pattern, and (safety) properties.



Monday, March 13, 2017

Clafer, ClaferIG, ClaferWiki 0.4.5 Released

by Michał Antkiewicz, Mar 13, 2017

This is mainly a maintenance release.


Clafer compiler, release pull request (0.4.5).
  • compatibility with GHC 8.0.2,
  • fixed an issue with references to singleton clafers in Choco generator.
Alloy-based instance generator, release pull request (0.4.5).
  • compatibility with GHC 8.0.2,
  • compatibility with clafer-0.4.5.
Claferwiki, release pull request (0.4.5).
  • compatibility with GHC 8.0.2,
  • compatibility with clafer-0.4.5 and the latest gitit-0.12.2.1
ClaferToolsST, release commit (0.4.5).
  • updated Package Control installation instructions for the latest SublimeText3.

All other tools work with 0.4.5.

Monday, September 19, 2016

Clafer Tools 0.4.4 Released

by Michał Antkiewicz, Sep 19, 2016

This is a simultaneous release of all Clafer Tools.

Binary builds are available from Clafer Tools - Binary Distributions.

Clafer compiler, release pull request (0.4.4).
  • compatibility with GHC 8.0.1,
  • added support for nested abstract clafers to Choco generator,
  • fixed building with latest Alex and Happy,
  • fixed an issue with setting references with a union, #49,
  • add the synthetic "root", #57,
  • added partial support for `parent` of top-level abstract clafers (the model now compiles but the generators must be fixed), #84.
Alloy-based instance generator, release pull request (0.4.4).
  • compatibility with GHC 8.0.1.
Choco-based instance generator and multi-objective optimizer, release pull request (0.4.4).
  • a massive update of 249 commits and 460 files changed!
  • ported to the latest Choco version 4.0,
  • added support for reference refinement, 
  • improved support for nested abstract clafers: issues #23, #29, #30, #31.
  • many performance improvements,
  • implemented constructive disjunction optimization.
      Claferwiki, release pull request (0.4.4).
      • compatibility with GHC 8.0.1,
      • compatibility with clafer-0.4.4 and the latest gitit-0.12.1.1
      ClaferToolsUICommonPlatform, release pull request (0.4.4).
      • fixed FQ matrix (fixed sorting, fixed references)
      • fixed Clafer API
      ClaferMOOVisualizer, release pull request (0.4.4).
      • minor fixes
      ClaferConfigurator, release diff (0.4.4).

      ClaferIDE, release diff (0.4.4).

      ClaferToolsST, release diff (0.4.4).
      • updated version numbers and links.
      ClaferMPS, release pull request (0.4.4).
      • added ability to extend the reference model with arbitrary clafers and constraints
      • added ability to add constraints to quality attributes
      • fixed quality table

      Tuesday, August 16, 2016

      Synthesis and Exploration of Multi-Level, Multi-Perspective Architectures of Automotive Embedded System

      by Michał Antkiewicz, Aug 16, 2016

      Jordan Ross' Masters thesis about using Clafer tools for synthesis and exploration of automotive architectures is now available for download:

      Synthesis and Exploration of Multi-Level, Multi-Perspective Architectures of Automotive Embedded System

      The models created in that work are available in GitHub repository ClaferCaseStudies.

      Monday, August 1, 2016

      Preprint of the ClaferMPS paper is available

      by Michał Antkiewicz, Aug 01, 2016

      The preprint of the paper 

      E. Khalilov, J. Ross, M. Antkiewicz, M. Voelter, and K. Czarnecki, "Modeling and Optimizing Automotive Electric/Electronic (E/E) Architectures: Towards Making Clafer Accessible to Practitioners", ISoLA, 2016

      is available for download.

      The paper describes features offered by the implementation of Clafer in JetBrains' Meta Programming System (MPS) and how it was used for modeling automotive E/E architectures. 

      The paper reflects ClaferMPS version 0.4.3. We are going to release ClaferMPS 0.4.4 soon, which adds exciting new features.

      Thursday, June 23, 2016

      Technical Report: Case Studies on E/E Architectures for Power Window and Central Door Locks Systems

      by Michał Antkiewicz, June 23, 2016

      Today, we published the final version of the technical report "Case Studies on E/E Architectures for Power Window and Central Door Locks Systems". The report contains:
      • An informal introduction to Clafer with sample outputs from the instance generator
      • Reference Model for E/E System Architecture for early design exploration including layers for feature model, functional analysis architecture, hardware design architecture (including communication and power topologies), and deployment.
      • Three case studies with lots of variability and many quality attributes (cost, mass, end-to-end latency):
        • Single door power window architecture
        • Two door power window architecture based on a generalized single door architecture
        • Central door locks architecture with remote key access and passive key entry
      • A set of techniques for modeling complex systems in Clafer
      The appendices contain
      • Appendix A Reference Model (148 lines)
      • Appendix B Generalized Single-Door Power Window (216 lines)
      • Appendix C Two-Door Power Window (184 lines)
      • Appendix D Central Door Locks (801 lines)
      For source code repositories and more information see the previous post.

      Friday, May 20, 2016

      ClaferMPS 0.4.3 Released

      by Michał Antkiewicz, May 20, 2016

      ClaferMPS is an implementation of Clafer in JetBrains Meta-Programming System (MPS). It also includes an Architecture DSL, which implements an adaptation of EAST-ADL reference model for early architecture modeling described in a technical report.

      ClaferMPS implements full Clafer 0.4.3 and provides
      • a smart structured editor with autocompletion and many intentions,
      • type system,
      • module system,
      • generator of plain-text Clafer.
      The Architecture DSL
      • technical feature model, functional analysis architecture, hardware design architecture, and separate functional to hardware architecture deployment specification,
      • editable textual and graphical projections,
      • semantic error checking according to the reference model,
      • separate definition of quality attributes,
      • generation of plain Clafer separate for every module with and without quality attributes.
      For installation and usage details, see README.

      Friday, May 13, 2016

      New automotive case studies in Clafer

      by Michał Antkiewicz, May 12, 2016

      We published a few new automotive body domain case studies in a GitHub repository 'ClaferCaseStudies'.

      Previously, the repository contained the original Power Window case study presented in Alexandr Murashkin's Master's thesis. Now, we added two new case studies by Jordan Ross: extended Power Window and Central Door Locks. More details in the README and the accompanying technical report.

      Additionally, we reimplemented the Power Window and Central Door Locks case studies in ClaferMPS. The MPS solutions are contained in MPS/Automotive/BodyDomain. We are in the process of releasing ClaferMPS and a separate announcement will follow.


      Tuesday, December 22, 2015

      Clafer Tools 0.4.3 Released

      by Michał Antkiewicz, Dec 22, 2015

      This is a simultaneous release of all Clafer Tools.

      Binary builds are available from Clafer Tools - Binary Distributions.

      Clafer compiler, release pull request (0.4.3).
      • added language feature with backend compatibility table,
      • added support for nested abstract clafers to Choco generator,
      • added checks for loops in inheritance hierarchy, issue 77,
      • fixed an issue with inheritance from a nested abstract clafer which itself has a superclafer, issue 78,
      • added min/max to Alloy generator, issue 79,
      • removed the unused and outdated python mode -m python,
      • fixed handling paths containing spaces in validation.
      Alloy-based instance generator, release pull request (0.4.3).
      • revised help messages, issue 28,
      • fix instance output to look like the original model to allow copy/paste from instance to the model for example-driven modeling.
      Choco-based instance generator and multi-objective optimizer, release pull request (0.4.3).
      • ported to the latest Choco3 version 3.3.3,
      • added support for nested abstract clafers,
      • added API for specifying ordering of clafers by giving priority branchingPriority([[a,b], [c,d], [e]]);,
      • improved performance, decreased solving time on a model from 247 minutes down to 9, see user's comment,
      • improved pretty printing of instances to harmonize with ClaferIG,
      • fixed multiplication/division and overflows handling,
      • fixed handling of zeroes in division.
          Claferwiki, release pull request (0.4.3).

          ClaferToolsUICommonPlatform.

          ClaferMOOVisualizer.

          ClaferConfigurator.

          ClaferIDE.

          ClaferToolsST, release diff (0.4.3).
          • fixed the problem with double quotes in tool path,
          • added a workaround for 32bit Java requirement on Windows for AlloyIG.

          Friday, November 20, 2015

          Backend Compatibility Matrix

          by Michał Antkiewicz

          We usually first implement new language features in one backend (e.g., Alloy) and add support to the other backend later. The result is that different backends support different language features.

          Therefore, we have created Backend Compatibility Matrix, which provides versions in which support for a given feature was added to Alloy-based and Choco-based backend.


          Tuesday, November 3, 2015

          Clafer Tools 0.4.2.1 Released

          by Michał Antkiewicz, updated on Nov 03, 2015

          This is a simultaneous release of all Clafer Tools.

          Binary builds are available from Clafer Tools - Binary Distributions.

          Clafer compiler, release pull request (0.4.2), hotfix (0.4.2.1).
          • added CheatSheet and generated syntax documentation clafer.pdf.
          • Added minimum and maximum of a set operators min and max.
          • Changed syntax of objectives to << minimize ... >> and << maximize ... >>. The old syntax << min ... >> and << max ... >> still works but it is now deprecated.
          • Changed precedence of if/then/else so that nested expressions do not need to be in parens. See issue #73.
          • Implemented ability for top-level abstract clafer to extend a nested abstract clafer #67. See test case.
          • Added generation of assertions for Choco.
          • Added validation with Choco and GraphVis to -v.
          • Use Haskell stack.
          Alloy-based instance generator, release pull request (0.4.2), hotfix (0.4.2.1).
          Choco-based instance generator and multi-objective optimizer, release pull request (0.4.2), release pull request (0.4.2.1).

          0.4.2
          0.4.2.1
          • Many optimizations
          • Improved symmetry breaking
          • Restore strategies "smaller" and "larger"
          • New command line options: time, noprint, dataFile
          • Ported to the latest Choco3/develop
          Claferwiki, release pull request (0.4.2), hotfix (0.4.2.1).
          ClaferToolsUICommonPlatform, release pull request (0.4.2).
          • Added excluding variants in the feature and quality matrix, issue #23.
          ClaferMOOVisualizer, release pull request (0.4.2).
          • Added excluding variants in the feature and quality matrix, issue #23.
          ClaferConfigurator, release diff (0.4.2).
          • Added excluding variants in the feature and quality matrix, issue #23.
          ClaferIDE, release diff (0.4.2).

          ClaferToolsST, release diff (0.4.2), release commit 0.4.2.1.

          Tuesday, October 27, 2015

          Example: Directed Graph Reachability in Presence of Variability

          by Michał Antkiewicz, updated on Oct 27, 2015

          With the features recently introduced to Clafer 0.4.1 (nested abstract clafers and reference refinement, see Clafer 0.4.0 PowerPoint Slide Show, and Alloy and Choco escapes), we can now conveniently model directed graphs in Clafer and express constraints such as node reachability in a graph by escaping to Alloy.

          On Oct 26, 2015, I gave a talk on the topic. Slides in PPSX. Slides in PDF.

          The talk was based on the wiki page

          Directed Graph Reachability in Presence of Variability

          on Clafer Model Wiki shows an example.