Bug 619831

Summary: Review Request: ltl2ba - Fast translation from LTL formulas to Büchi automata
Product: [Fedora] Fedora Reporter: David A. Wheeler <dwheeler>
Component: Package ReviewAssignee: Mark Rader <msrader>
Status: CLOSED ERRATA QA Contact: Fedora Extras Quality Assurance <extras-qa>
Severity: medium Docs Contact:
Priority: medium    
Version: rawhideCC: fedora-package-review, msrader, notting
Target Milestone: ---Flags: msrader: fedora-review+
kevin: fedora-cvs+
Target Release: ---   
Hardware: All   
OS: Linux   
Whiteboard:
Fixed In Version: ltl2ba-1.1-2.fc14 Doc Type: Bug Fix
Doc Text:
Story Points: ---
Clone Of: Environment:
Last Closed: 2010-08-06 20:55:23 UTC Type: ---
Regression: --- Mount Type: ---
Documentation: --- CRM:
Verified Versions: Category: ---
oVirt Team: --- RHEL 7.3 requirements from Atomic Host:
Cloudforms Team: --- Target Upstream Version:
Embargoed:

Description David A. Wheeler 2010-07-30 16:22:47 UTC
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 19:01:11 UTC
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 11:21:00 UTC
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 18:19:44 UTC
"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 18:42:37 UTC
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 11:27:33 UTC
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 11:35:12 UTC
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 11:19:57 UTC
David

The rest of the package seems fine.  I will mark it as upload.

Comment 8 David A. Wheeler 2010-08-05 01:40:00 UTC
Great! Thanks for the review.

Comment 9 David A. Wheeler 2010-08-05 01:45:32 UTC
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 17:09:04 UTC
Git done (by process-git-requests).

Comment 11 Fedora Update System 2010-08-05 22:22:26 UTC
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 22:22:33 UTC
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 22:22:38 UTC
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 20:55:18 UTC
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 20:56:19 UTC
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-19 01:07:53 UTC
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.