From mboxrd@z Thu Jan 1 00:00:00 1970 Path: news.gmane.io!.POSTED.blaine.gmane.org!not-for-mail From: Nala Ginrut Newsgroups: gmane.lisp.guile.user Subject: Re: [ANN] Dezyne 2.15.0 released as Free Software Date: Sat, 7 May 2022 01:23:33 +0800 Message-ID: References: <87r156n70n.fsf@gnu.org> Mime-Version: 1.0 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Injection-Info: ciao.gmane.io; posting-host="blaine.gmane.org:116.202.254.214"; logging-data="40169"; mail-complaints-to="usenet@ciao.gmane.io" Cc: dezyne-devel@nongnu.org, Guile User To: Jan Nieuwenhuizen Original-X-From: guile-user-bounces+guile-user=m.gmane-mx.org@gnu.org Fri May 06 19:24:14 2022 Return-path: Envelope-to: guile-user@m.gmane-mx.org Original-Received: from lists.gnu.org ([209.51.188.17]) by ciao.gmane.io with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.92) (envelope-from ) id 1nn1gb-000AEa-95 for guile-user@m.gmane-mx.org; Fri, 06 May 2022 19:24:13 +0200 Original-Received: from localhost ([::1]:59400 helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1nn1gZ-0000ff-SH for guile-user@m.gmane-mx.org; Fri, 06 May 2022 13:24:11 -0400 Original-Received: from eggs.gnu.org ([2001:470:142:3::10]:52240) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1nn1gH-0000fP-JY for guile-user@gnu.org; Fri, 06 May 2022 13:23:53 -0400 Original-Received: from mail-ej1-x62a.google.com ([2a00:1450:4864:20::62a]:39565) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1nn1gE-0005yO-2A; Fri, 06 May 2022 13:23:53 -0400 Original-Received: by mail-ej1-x62a.google.com with SMTP id bv19so15708356ejb.6; Fri, 06 May 2022 10:23:47 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112; h=mime-version:references:in-reply-to:from:date:message-id:subject:to :cc; bh=gJH6L5G7Rx4heleFLI7LT5Kb+MBdlqLI1fs6xfxyViA=; b=VK7apEqTb3BPV1TkB01lnFz/Hr62zIeO+qLqru6c6T4xUD27MfTUkatTjpY/X3MvF6 2QHiK7rqA2QDCNgoCTrwsOw3iCo4RUCtA6eAO9OhnLJCE1QTJEfWezLTedzU4Yb80biF 4cPY+tMULEWc8ZpIElbt20f2QNextr7De8aqh6X8B4ZTnx1J5cuQDNDaoA5ZTgr6ByBM GuhgtPdFC1iz/0sLIg1UbDo9z0T35Q3/xH8m48tKrR/E176ynx7eb9wDbWA313lEi14X BMGXuYBNO7CCJhXYMBl1HQ71/TXAcKznFiNIw/acuExuS3SU0t9OOi9NjKkOucgt/cxy K7mw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=x-gm-message-state:mime-version:references:in-reply-to:from:date :message-id:subject:to:cc; bh=gJH6L5G7Rx4heleFLI7LT5Kb+MBdlqLI1fs6xfxyViA=; b=uoZqUPxbWBrGkzN/qZXxZKiIeqOeiHWvt65phV6CdA/98hwywVr09rnov5VpqjdxVR IdibW4JrqG/timH441DB36aPZpIdq0Fn97w8q7myDYZtOOUzZDHafT7X7JDipoTT1hY9 DX2omW8PiGtTui9sL169OnnutKwHTJ/msPIayctLN48QMH/ioJsMVubcCQbhdzqLRQdd 8Zd9y43n17oj4vRR6pKpJLYPfx1iG6eut7co6G+PkrNoPdU6vQNrRIhGl3Hu0Z2XsTCE 0O1JJD+ksfKCMVXUmpxJZkKNaMnUXczcd2b7f3UIkpy840wNZwmeOscdA9zFoUAe3+LA XhFQ== X-Gm-Message-State: AOAM530XP5jZ2XeKr5OJrt9S9f3x7aV9FSwPKcJNuzxfmdRzbH73cPBZ a+AuPzZz+KjXLpMLK+YoQTOny93tt2E2xLLf/0ETrVws X-Google-Smtp-Source: ABdhPJwt1HXBISoeSJXDJQqMchQvHyvOZBc8hPjT0U/MaW8dcrofQ4vOIL+b8GRJq7DBex951rUCMvTjt62jSUtyeNk= X-Received: by 2002:a17:907:1b1f:b0:6f0:21ec:6051 with SMTP id mp31-20020a1709071b1f00b006f021ec6051mr3693979ejc.533.1651857825932; Fri, 06 May 2022 10:23:45 -0700 (PDT) In-Reply-To: <87r156n70n.fsf@gnu.org> Received-SPF: pass client-ip=2a00:1450:4864:20::62a; envelope-from=nalaginrut@gmail.com; helo=mail-ej1-x62a.google.com X-Spam_score_int: -20 X-Spam_score: -2.1 X-Spam_bar: -- X-Spam_report: (-2.1 / 5.0 requ) BAYES_00=-1.9, DKIM_SIGNED=0.1, DKIM_VALID=-0.1, DKIM_VALID_AU=-0.1, DKIM_VALID_EF=-0.1, FREEMAIL_FROM=0.001, HTML_MESSAGE=0.001, RCVD_IN_DNSWL_NONE=-0.0001, SPF_HELO_NONE=0.001, SPF_PASS=-0.001, T_SCC_BODY_TEXT_LINE=-0.01 autolearn=unavailable autolearn_force=no X-Spam_action: no action X-Content-Filtered-By: Mailman/MimeDel 2.1.29 X-BeenThere: guile-user@gnu.org X-Mailman-Version: 2.1.29 Precedence: list List-Id: General Guile related discussions List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: guile-user-bounces+guile-user=m.gmane-mx.org@gnu.org Original-Sender: "guile-user" Xref: news.gmane.io gmane.lisp.guile.user:18266 Archived-At: It's really nice!! On Fri, May 6, 2022, 21:09 Jan Nieuwenhuizen wrote: > We are thrilled to announce Dezyne 2.15: Dezyne is now being released as > Free Software (FLOSS). > > * About > > Dezyne[0] is a programming language and a set of tools to specify, > validate, verify, simulate, document, and implement concurrent control > software. > > The Dezyne language has formal semantics expressed in mCRL2[1] developed = at > the department of Mathematics and Computer Science of the Eindhoven > University of Technology (TUE[2]). Dezyne requires that every model is > finite, deterministic and free of deadlocks, livelocks, and contract > violations. This achieved by means of the language itself as well as > by builtin verification through model checking. This allows the > construction of complex systems by assembling independently verified > components. > > * Summary > > This release completes full support for blocking: This finally marks > the Grand Unification into single threaded execution semantics. > > The documentation has seen a major rewrite and is available here: > . > > We will evaluate your reports and track them via the > Gitlab dezyne-issues project[3], see our guide to writing > helpful bug reports[4]. > > * What's next? > > Verification with system scope and automatically exploring possible > traces in a system. Introducing a new keyword `defer' for asynchronous > behavior and deprecation of `async'. > > * Future > > Looking beyond the next releases we will introduce implicit interface > constraints. Hierarchical behaviors, module-specifications and > data-interfaces. Support for Model Based Testing. > > Please do not hesitate to forward this announcement to other fora > interested in formal methods and verification! > > Enjoy! > The Dezyne developers. > > * Download > > git clone git://git.savannah.nongnu.org/dezyne.git > > Here are the compressed sources and a GPG detached signature[*]: > https://dezyne.org/download/dezyne/dezyne-2.15.0.tar.gz > https://dezyne.org/download/dezyne/dezyne-2.15.0.tar.gz.sig > > Here are the SHA1 and SHA256 checksums: > > 395ff05e4f2c17bcee895fd9436d696fb0aab93d dezyne-2.15.0.tar.gz > 982d8f7cca9de23225e2f06b4c8524c0b57acfba81beaaff1a0c045c1e6409ea > dezyne-2.15.0.tar.gz > > [*] Use a .sig file to verify that the corresponding file (without the > .sig suffix) is intact. First, be sure to download both the .sig file > and the corresponding tarball. Then, run a command like this: > > gpg --verify dezyne-2.15.0.tar.gz.sig > > If that command fails because you don't have the required public key, > then run this command to import it: > > gpg --keyserver keys.gnupg.net --recv-keys > 1A858392E331EAFDB8C27FFBF3C1A0D9C1D65273 > > and rerun the 'gpg --verify' command. > > Alternatively, Dezyne can be installed using GNU Guix[5]: > guix pull > guix install dezyne > > * NEWS > > * Changes in 2.15.0 since 2.14.0 > ** Language > - Blocking is now fully supported, it may be used: > + In non-toplevel components, > + In a component with multiple provides ports, but see the > `Blocking' section in the manual for caveats. > + A new `blocking' qualifier for ports must be used if a port can > block, or block collateraly. > - Using unobservable non-determinism in interfaces is no longer > supported. > - An action or function call can now also be used in a return > expression (#67[5]). Note that recursive functions still cannot be > valued. > ** Commands > - The `dzn explore' command has been removed. > ** Verification > - The verifier now supports blocking for components with multiple > provides ports. > - The verifier now detects possible deadlock errors due to a requires > action blocking collaterally, which could happen when a component > deeper in the system hierarchy uses blocking. > - The option `--no-interface-determinism' has been removed for `dzn > verify'. > ** Simulation > - The simulator now supports collateral blocking. > - In interactive mode: > + The new `,state' command shows the state (#66[6]), > + The new `,quit' command exits the session, > + The simulator does not exit when supplying empty input. > - The simulator now detects possible deadlock errors due to a requires > action blocking collaterally, which could happen when a component > deeper in the system hierarchy uses blocking. > - The simulator now detects livelocks in interfaces at end of trail. > - The simulator now detects queue-full errors caused by external at > end of trail. > - The `dzn simulate' command now supports the `-C,--no-compliance', > `--no-interface-livelock' and `-Q,--no-queue-full' options, > ** Code > - The C++ and C# code generators and runtime now fully support > collaterally blocking components. > ** Views > - Returns are no longer removed from the state-diagram. Using the new > `--hide=3Dreturns' (or `--hide=3Dactions') now removes void action > returns. > ** Documentation > - Blocking has been updated and extended. > - A new section on foreign components was added. > ** Noteworthy bug fixes > - Using the construct `provides external' (which has no semantics) no > longer confuses the simulator. > - A bug has been fixed that would cause the well-welformness check for > system bindings to ignore certain missing bindings. > - A bug has been fixed when assigning a value to a formal parameter of > a function. > - A bug has been fixed in the vm that would cause graph or simulate to > hang when using a foreign component that has both provides and > requires ports (note: don't do that!). > - The test framework can be built using gcc-11. > - A bug has been fixed in the code generator when assiging to a local > variable that shadows a formal parameter or member variable. > - A bug has been fixed in the verifier when creating a new local > variable or assigning a variable that remains otherwise unused. > - The simulation function now supports injection of foreign > components. > - The trace produced by running dezyne code is now correct when using > injected foreign components. > - A bug has been fixed that would cause the verifier to overlook > non-determinism in a component. > - Using external data in binary expressions is now reported as an > error (#64[7]). > - The parser no longer reports "" expected when an > external type definition is missing. > - The well-formedness check of the parser no longer hangs when a > component has the same name as one of its interfaces. > - An interface can now have the same name as its namespace. > > * Links > > [0] https://dezyne.org > [1] https://mcrl2.org > [2] https://tue.nl > [3] https://gitlab.com/groups/dezyne/-/issues > [4] https://dezyne.org/bugreport > [5] https://gitlab.com/dezyne/dezyne-issues/-/issues/67 > [6] https://gitlab.com/dezyne/dezyne-issues/-/issues/66 > [7] https://gitlab.com/dezyne/dezyne-issues/-/issues/61 > > -- > Jan Nieuwenhuizen | GNU LilyPond https://lilypond.org > Freelance IT https://JoyOfSource.com | Avatar=C2=AE https://AvatarAcademy= .com > >