Bugzilla will be upgraded to version 5.0 on December 2, 2018. The outage period for the upgrade will start at 0:00 UTC and have a duration of 12 hours
Bug 619831 - Review Request: ltl2ba - Fast translation from LTL formulas to Büchi automata
Review Request: ltl2ba - Fast translation from LTL formulas to Büchi automata
Status: CLOSED ERRATA
Product: Fedora
Classification: Fedora
Component: Package Review (Show other bugs)
rawhide
All Linux
medium Severity medium
: ---
: ---
Assigned To: Mark Rader
Fedora Extras Quality Assurance
:
Depends On:
Blocks:
  Show dependency treegraph
 
Reported: 2010-07-30 12:22 EDT by David A. Wheeler
Modified: 2010-08-18 21:07 EDT (History)
3 users (show)

See Also:
Fixed In Version: ltl2ba-1.1-2.fc14
Doc Type: Bug Fix
Doc Text:
Story Points: ---
Clone Of:
Environment:
Last Closed: 2010-08-06 16:55:23 EDT
Type: ---
Regression: ---
Mount Type: ---
Documentation: ---
CRM:
Verified Versions:
Category: ---
oVirt Team: ---
RHEL 7.3 requirements from Atomic Host:
Cloudforms Team: ---
msrader: fedora‑review+
kevin: fedora‑cvs+


Attachments (Terms of Use)

  None (edit)
Description David A. Wheeler 2010-07-30 12:22:47 EDT
Spec URL: http://www.dwheeler.com/SPECS/ltl2ba.spec
SRPM URL:  http://www.dwheeler.com/SRPMS/ltl2ba-1.1-1.fc13.src.rpm
Description:

Translate from Linear temporal logic (LTL) formulas to Büchi automata.
LTL is a type of formal logic that extends formal logic with
qualifiers involving time.
A Büchi automaton is the extension of a finite state automaton
to infinite inputs, and are useful for specifying behavior
of non-terminating systems (such as hardware or operating systems).
A Büchi automaton accepts an infinite input sequence if and only if
there exists a run of the automaton which visits at least one of the
final states infinitely often.

The implementation is based on the translation algorithm by Gastin and Oddoux,
presented at the CAV Conference, held in 2001, Paris, France 2001.

This package is a useful extension for Frama-C.
Comment 1 David A. Wheeler 2010-07-30 15:01:11 EDT
FYI, an rpmlint (using 32-bit Fedora 13) produces 0 errors and 5 warnings, and none of the warnings should inhibit distribution.

Of the 5 warnings, 4 of them are because the Fedora spellchecker's wordlist does not include the word "automata".  Since "automata" is the correct word, those warnings are irrelevant.  The other warning complains that there's no manual page.  Unfortunately, the upstream package doesn't include a manual page, so I don't have one to package.  The program does include a help option, in case that's any consolation.

$ rpmlint ltl2ba.spec ../SRPMS/ltl2ba-1.1-1.fc13.src.rpm ../RPMS/i686/ltl2ba-*

ltl2ba.src: W: spelling-error Summary(en_US) automata -> automats, automat, automate
ltl2ba.src: W: spelling-error %description -l en_US automata -> automats, automat, automate
ltl2ba.i686: W: spelling-error Summary(en_US) automata -> automats, automat, automate
ltl2ba.i686: W: spelling-error %description -l en_US automata -> automats, automat, automate
ltl2ba.i686: W: no-manual-page-for-binary ltl2ba
3 packages and 1 specfiles checked; 0 errors, 5 warnings.
Comment 2 Mark Rader 2010-08-02 07:21:00 EDT
Initial Comments:

Need to correct spelling/fonts in the Spec File.  Büchi is probably the correct spelling but it uses fonts that do not display well and can cause issues.

MUST: rpmlint must be run on every package. The output should be posted in the review.

(Done)

MUST: The package must be named according to the Package Naming Guidelines .

(Ok)

MUST: The spec file name must match the base package %{name}, in the format %{name}.spec unless your package has an exemption.

(Ok) 

MUST: The package must meet the Packaging Guidelines .

(Ok)

MUST: The package must be licensed with a Fedora approved license and meet the Licensing Guidelines .

(Ok)

MUST: The License field in the package spec file must match the actual license. 

(Ok)

MUST: If (and only if) the source package includes the text of the license(s) in its own file, then that file, containing the text of the license(s) for the package must be included in %doc.[4]

MUST: The spec file must be written in American English. [5]
(Issue, contains non english characters)

MUST: The spec file for the package MUST be legible. [6]
(Issue, contails non ascii characters)

MUST: The sources used to build the package must match the upstream source, as provided in the spec URL. Reviewers should use md5sum for this task. If no upstream URL can be specified for this package, please see the Source URL Guidelines for how to deal with this.
(Ok)

MUST: The package MUST successfully compile and build into binary rpms on at least one primary architecture. [7]
(Unknown Koji Build is needed)

MUST: If the package does not successfully compile, build or work on an architecture, then those architectures should be listed in the spec in ExcludeArch. Each architecture listed in ExcludeArch MUST have a bug filed in bugzilla, describing the reason that the package does not compile/build/work on that architecture. The bug number MUST be placed in a comment, next to the corresponding ExcludeArch line. [8]
(Unknown Koji Build is needed)

MUST: All build dependencies must be listed in BuildRequires, except for any that are listed in the exceptions section of the Packaging Guidelines ; inclusion of those as BuildRequires is optional. Apply common sense.
(Unknown Koji Build is needed)

MUST: The spec file MUST handle locales properly. This is done by using the %find_lang macro. Using %{_datadir}/locale/* is strictly forbidden.[9]

MUST: Every binary RPM package (or subpackage) which stores shared library files (not just symlinks) in any of the dynamic linker's default paths, must call ldconfig in %post and %postun. [10]
(Ok)

MUST: Packages must NOT bundle copies of system libraries.[11]
(Ok)


MUST: A package must own all directories that it creates. If it does not create a directory that it uses, then it should require a package which does create that directory.
(Ok)
Comment 3 David A. Wheeler 2010-08-02 14:19:44 EDT
"Büchi" is the correct spelling, with the second letter as "u umlaut", and it's okay to use UTF-8 to encode such letters. But obviously that causes some problems for you, so I will change it.

The two main alternative spellings are "Buchi" and "Buechi".  Wikipedia accepts them both.  A Google search for "Buchi automata" returned about 8,600 entries, while "Beuchi automata" returned 889 results.  Since  "Buchi automata" seems to be far more common, I'll switch to that.

Any other changes you'd like to see?
Comment 4 Mark Rader 2010-08-02 14:42:37 EDT
David

We really need the koji build to finish.  This is for the folling requirements.

MUST: If the package does not successfully compile, build or work on an
architecture, then those architectures should be listed in the spec in
ExcludeArch. Each architecture listed in ExcludeArch MUST have a bug filed in
bugzilla, describing the reason that the package does not compile/build/work on
that architecture. The bug number MUST be placed in a comment, next to the
corresponding ExcludeArch line. [8]
(Unknown Koji Build is needed to test)

MUST: All build dependencies must be listed in BuildRequires, except for any
that are listed in the exceptions section of the Packaging Guidelines ;
inclusion of those as BuildRequires is optional. Apply common sense.
(Unknown Koji Build is needed to test)

Also as noted from the reviewers package, you fixed it, but this is why I am harping.

MUST: The spec file must be written in American English. [5]
(Issue, contains non english characters)

MUST: The spec file for the package MUST be legible. [6]
(Issue, contails non ascii characters)
Comment 5 Mark Rader 2010-08-03 07:27:33 EDT
David

MUST: The package MUST successfully compile and build into binary rpms on at
least one primary architecture. [7]
(Koji Worked)

MUST: If the package does not successfully compile, build or work on an
architecture, then those architectures should be listed in the spec in
ExcludeArch. Each architecture listed in ExcludeArch MUST have a bug filed in
bugzilla, describing the reason that the package does not compile/build/work on
that architecture. The bug number MUST be placed in a comment, next to the
corresponding ExcludeArch line. [8]
(Koji Worked)

MUST: All build dependencies must be listed in BuildRequires, except for any
that are listed in the exceptions section of the Packaging Guidelines ;
inclusion of those as BuildRequires is optional. Apply common sense.
(Koji Worked))

MUST: The spec file MUST handle locales properly. This is done by using the
%find_lang macro. Using %{_datadir}/locale/* is strictly forbidden.

(Ok)
Comment 6 Mark Rader 2010-08-03 07:35:12 EDT
David

MUST: Every binary RPM package (or subpackage) which stores shared library files (not just symlinks) in any of the dynamic linker's default paths, must call ldconfig in %post and %postun. 
(N/A)

MUST: Packages must NOT bundle copies of system libraries.
(Ok)

MUST: If the package is designed to be relocatable, the packager must state this fact in the request for review, along with the rationalization for relocation of that specific package. Without this, use of Prefix: /usr is considered a blocker.
(N/A)

MUST: A package must own all directories that it creates. If it does not create a directory that it uses, then it should require a package which does create that directory.
(Ok)

MUST: A Fedora package must not list a file more than once in the spec file's %files listings. (Notable exception: license texts in specific situations)
(Ok)
Comment 7 Mark Rader 2010-08-04 07:19:57 EDT
David

The rest of the package seems fine.  I will mark it as upload.
Comment 8 David A. Wheeler 2010-08-04 21:40:00 EDT
Great! Thanks for the review.
Comment 9 David A. Wheeler 2010-08-04 21:45:32 EDT
New Package SCM Request
=======================
Package Name: ltl2ba
Short Description: Fast translation from LTL formulas to Buchi automata
Owners: dwheeler mrader
Branches: f12 f13 f14
InitialCC:
Comment 10 Kevin Fenzi 2010-08-05 13:09:04 EDT
Git done (by process-git-requests).
Comment 11 Fedora Update System 2010-08-05 18:22:26 EDT
ltl2ba-1.1-2.fc13 has been submitted as an update for Fedora 13.
http://admin.fedoraproject.org/updates/ltl2ba-1.1-2.fc13
Comment 12 Fedora Update System 2010-08-05 18:22:33 EDT
ltl2ba-1.1-2.fc12 has been submitted as an update for Fedora 12.
http://admin.fedoraproject.org/updates/ltl2ba-1.1-2.fc12
Comment 13 Fedora Update System 2010-08-05 18:22:38 EDT
ltl2ba-1.1-2.fc14 has been submitted as an update for Fedora 14.
http://admin.fedoraproject.org/updates/ltl2ba-1.1-2.fc14
Comment 14 Fedora Update System 2010-08-06 16:55:18 EDT
ltl2ba-1.1-2.fc13 has been pushed to the Fedora 13 stable repository.  If problems still persist, please make note of it in this bug report.
Comment 15 Fedora Update System 2010-08-06 16:56:19 EDT
ltl2ba-1.1-2.fc12 has been pushed to the Fedora 12 stable repository.  If problems still persist, please make note of it in this bug report.
Comment 16 Fedora Update System 2010-08-18 21:07:53 EDT
ltl2ba-1.1-2.fc14 has been pushed to the Fedora 14 stable repository.  If problems still persist, please make note of it in this bug report.

Note You need to log in before you can comment on or make changes to this bug.