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.


      Friday, October 2, 2015

      Clafer Cheat Sheet and Syntax Documentation

      by Michał Antkiewicz

      Clafer has a formal grammar from which the lexer and parser are generated. I published two new language reference resources: 
      • Syntax documentation (pdf), which is also automatically generated from the grammar
      • Clafer cheat sheet, which is written manually based on the grammar to provide additional commentary and type information, while sacrificing the formality of the grammar.
      All these resources, as of this posting, cover Clafer 0.4.1 and they will be updated with each release. They are also referenced from the page Documentation.

      Monday, September 21, 2015

      Clafer Web Tools 0.4.1 Released

      by Michał Antkiewicz

      The release 0.4.1 of the web tools is the first major release since 0.3.6.1!

      This release wouldn't be possible without the hard work of Eldar Khalilov who took on a difficult task of switching the tools from the old XML format to the new JSON format of the compiler's intermediate representation.

      The release includes compatibility with Clafer 0.4.1 and the new features of the language since 0.3.6.1 and many functional and performance improvements (by both Alexandr Murashkin and Eldar Khalilov).

      Tuesday, September 1, 2015

      Clafer, ClaferIG, and ClaferWiki 0.4.1 Released

      by Michał Antkiewicz

      Clafer compiler, Alloy-based instance generator, and wiki 0.4.1 are released on Hackage (claferclaferIGclaferwiki). The release also includes the Choco3-based instance generator and optimizer 0.4.0, which; however, does not yet support the new features of the language.

      Binary builds are available from Clafer Tools - Binary Distributions.

      See the corresponding release 0.4.1 of the web tools.


      Major changes include:
      • Fixed problems with automatic dereferencing, see leftAssocDeref.cfr, navAndDeref.cfr, and navAndDeref.als.reg.
      • Fixed type system problems. 
      • Added Alloy and Choco escapes, see escapes.cfr. Code in Alloy escapes is included at the beginning of the Alloy output, whereas, Choco escapes are included at the end of Choco output. 
      • Changed ref to dref. 
      • Added handling and deprecation warnings for deprecated ref and &; instead dref and ** should be used, see deprecated.cfr
      • Fixed bugs with incorrect addition of .drefs in arithmetic, see arithmetic.cfr
      • Fixed missing links bugs in HTML output. 
      • Added continuous integration with TravisCI.
      For details, see Clafer Release 0.4.1 Pull Request.

      Previous release Clafer, ClaferIG, ClaferWiki, ChocoSolver, and ClaferChocoIG 0.4.0 Released.