fstds System: A fuzzy-set manipulation system

This paper describes an implementation of a system for fuzzy sets manipulation which is based on fstds (Fuzzy-Set-Theoretic Data Structure), an extended version of Childs's stds (Set-Theoretic Data Structure). The fstds language is considered as a fuzzy-set-theoretically oriented language which can deal, for example, with ordinary sets, ordinary relations, fuzzy sets, fuzzy relations, L-fuzzy sets, level-m fuzzy sets and type-n fuzzy sets. The system consists of an interpreter, a collection of fuzzy-set operations and the data structure, fstds, for representing fuzzy sets. fstds is made up of eight areas, namely, the fuzzy-set area, fuzzy-set representation area, grade area, grade-tuple area, element area, element-tuple area, fuzzy-set name area and fuzzy-set operator name area. The fstds system, in which 52 fuzzy-set operations are available, is implemented in fortran, and is currently running on a FACOM 230-45S computer.     

Software specification using the special language

This paper presents a tutorial overview of special, a formal specification and assertion language created by SRI International as part of their hierarchical design methodology. The language is based on a formal model of system behavior and is supported by language processors that assist in the interactive development of specifications. special is a strongly typed language that models data and programs as abstract resources known as objects. Collections of modules known as abstract machines are the major building blocks of a software specification in special. The technical foundations of special and the components of a special specification are described. A sample specification is detailed in an appendix.     

TiReX: Replica-exchange molecular dynamics using Tinker

We present a driver program for performing replica-exchange molecular dynamics simulations with the Tinker package. Parallelization is based on the Message Passing Interface, with every replica assigned to a separate process. The algorithm is not communication intensive, which makes the program suitable for running even on loosely coupled cluster systems. Particular attention is paid to the practical aspects of analyzing the program output.

Program summary

Program title: TiReXCatalogue identifier: AEEK_v1_0Program summary URL:http://cpc.cs.qub.ac.uk/summaries/AEEK_v1_0.htmlProgram obtainable from: CPC Program Library, Queen's University, Belfast, N. IrelandLicensing provisions: Standard CPC licence, http://cpc.cs.qub.ac.uk/licence/licence.htmlNo. of lines in distributed program, including test data, etc.: 43 385No. of bytes in distributed program, including test data, etc.: 502 262Distribution format: tar.gzProgramming language: Fortran 90/95Computer: Most UNIX machinesOperating system: LinuxHas the code been vectorized or parallelized?: parallelized with MPIClassification: 16.13External routines: TINKER version 4.2 or 5.0, built as a libraryNature of problem: Replica-exchange molecular dynamics.Solution method: Each replica is assigned to a separate process; temperatures are swapped between replicas at regular time intervals.Running time: The sample run may take up to a few minutes.     

Working with occam: a program for generating display images

It is assumed that a host processor computes the corner coordinates of surfaces and outputs these sequentially, in ranked order, to the components described in an OCCAM program. The data is precomputed and stored in a sequential file. A scheduler controls the activity of a number of zone management processors (ZMPs), all running in parallel, and a special memory buffer. Each ZMP handles only one surface at a time. A processor can pick up a new surface for display when the previous surface has been completed. Only one ZMP can write into a given raster scanline at one time. Others may be writing into the same column of other lines at the same time. Hidden surface elimination is achieved by processing the surfaces in an order ranked on distance from the viewing point. This ranking is done in the host processor. The ranked data is held on a file, which is read sequentially in 512 byte blocks. This data has been previously computed and stored as a sequence of double-byte integers in the required order for a series of picture frames, one frame per 512 byte block. The occam implementation on the Apple II europlus running under UCSD version 4 is very slow. It is postulated that an implementation using separate occam professor hardware units for each appropriate process would run in real time. There is considerable communication between the processors. The activity of each processor is generally sequential and all the processors run in parallel. Comments are made about some of the problems and advantages of programming in occam in an appendix.     

PVS#: Streamlined Tacticals for PVS

The semantics of a proof language relies on the representation of the state of a proof after a logical rule has been applied. This information, which is usually meaningless from a logical point of view, is fundamental to describe the control mechanism of the proof search provided by the language. In this paper, we present a monadic datatype to represent the state information of a proof and we illustrate its use in the PVS theorem prover. We show how this representation can be used to design a new set of powerful tacticals for PVS, called PVS#, that have a simpler and clearer semantics compared to the semantics of standard PVS tacticals.     

ReSpecT Nets: Towards an Analysis Methodology for ReSpecT Specifications

A key feature for infrastructures providing coordination services is the ability to define the behaviour of coordination abstractions according to the requirements identified at design-time. We take as a representative for this scenario the logic-based language ReSpecT (Reaction Specification Tuples), used to program the reactive behaviour of tuple centres. ReSpecT specifications are at the core of the engineering methodology underlying the TuCSoN infrastructure, and are therefore the “conceptual place” where formal methods can be fruitfully applied to guarantee relevant system properties.In this paper we introduce ReSpecT nets, a formalism that can be used to describe reactive behaviours that can succeed and fail, and that allows for an encoding to Petri nets with inhibitor arcs. ReSpecT nets are introduced to give a core model to a fragment of the ReSpecT language, and to pave the way for devising an analysis methodology including formal verification of safety and liveness properties. In particular, we provide a semantics to ReSpecT specifications through a mapping to ReSpecT nets. The potential of this approach for the analysis of ReSpecT specifications is discussed, presenting initial results for the analysis of safety properties.     

Revised and extended Utilities for the Ratip package

During the last years, the Ratip package has been found useful for calculating the excitation and decay properties of free atoms. Based on the (relativistic) multiconfiguration Dirac-Fock method, this program is used to obtain accurate predictions of atomic properties and to analyze many recent experiments. The daily work with this package made an extension of its Utilities [S. Fritzsche, Comput. Phys. Comm. 141 (2001) 163] desirable in order to facilitate the data handling and interpretation of complex spectra. For this purpose, we make available an enlarged version of the Utilities which mainly supports the comparison with experiment as well as large Auger computations. Altogether 13 additional tasks have been appended to the program together with a new menu structure to improve the interactive control of the program.

Program summary

Title of program: RATIPCatalogue identifier: ADPD_v2_0Program summary URL:http://cpc.cs.qub.ac.uk/summaries/ADPD_v2_0Program obtainable from: CPC Program Library, Queen's University of Belfast, N. IrelandLicensing provisions: noneReference in CPC to previous version: S. Fritzsche, Comput. Phys. Comm. 141 (2001) 163Catalogue identifier of previous version: ADPDAuthors of previous version: S. Fritzsche, Department of Physics, University of Kassel, Heinrich-Plett-Strasse 40, D-34132 Kassel, GermanyDoes the new version supersede the original program?: yesComputer for which the new version is designed and others on which it has been tested: IBM RS 6000, PC Pentium II-IVInstallations: University of Kassel (Germany), University of Oulu (Finland)Operating systems: IBM AIX, Linux, UnixProgram language used in the new version: ANSI standard Fortran 90/95Memory required to execute with typical data: 300 kBNo. of bits in a word: All real variables are parameterized by a selected kind parameter and, thus, can be adapted to any required precision if supported by the compiler. Currently, the kind parameter is set to double precision (two 32-bit words) as used also for other components of the Ratip package [S. Fritzsche, C.F. Fischer, C.Z. Dong, Comput. Phys. Comm. 124 (2000) 341; G. Gaigalas, S. Fritzsche, Comput. Phys. Comm. 134 (2001) 86; S. Fritzsche, Comput. Phys. Comm. 141 (2001) 163; S. Fritzsche, J. Elec. Spec. Rel. Phen. 114-116 (2001) 1155]No. of lines in distributed program, including test data, etc.:231 813No. of bytes in distributed program, including test data, etc.: 3 977 387Distribution format: tar.gzip fileNature of the physical problem: In order to describe atomic excitation and decay properties also quantitatively, large-scale computations are often needed. In the framework of the Ratip package, the Utilities support a variety of (small) tasks. For example, these tasks facilitate the file and data handling in large-scale applications or in the interpretation of complex spectra.Method of solution: The revised Utilities now support a total of 29 subtasks which are mainly concerned with the manipulation of output data as obtained from other components of the Ratip package. Each of these tasks are realized by one or several subprocedures which have access to the corresponding modules of the main components. While the main menu defines seven groups of subtasks for data manipulations and computations, a particular task is selected from one of these group menus. This allows to enlarge the program later if technical support for further tasks will become necessary. For each selected task, an interactive dialog about the required input and output data as well as a few additional information are printed during the execution of the program.Reasons for the new version: The requirement for enlarging the previous version of the Utilities [S. Fritzsche, Comput. Phys. Comm. 141 (2001) 163] arose from the recent application of the Ratip package for large-scale radiative and Auger computations. A number of new subtasks now refer to the handling of Auger amplitudes and their proper combination in order to facilitate the interpretation of complex spectra. A few further tasks, such as the direct access to the one-electron matrix elements for some given set of orbital functions, have been found useful also in the analysis of data.Summary of revisions: extraction and handling of atomic data within the framework of Ratip. With the revised version, we now ‘add’ another 13 tasks which refer to the manipulation of data files, the generation and interpretation of Auger spectra, the computation of various one- and two-electron matrix elements as well as the evaluation of momentum densities and grid parameters. Owing to the rather large number of subtasks, the main menu has been divided into seven groups from which the individual tasks can be selected very similarly as before.Typical running time: The program responds promptly for most of the tasks. The responding time for some tasks, such as the generation of a relativistic momentum density, strongly depends on the size of the corresponding data files and the number of grid points.Unusual features of the program: A total of 29 different tasks are supported by the program. Starting from the main menu, the user is guided interactively through the program by a dialog and a few additional explanations. For each task, a short summary about its function is displayed before the program prompts for all the required input data.     

Merging the autoview image processing language with prolog

A new computer language, called provision, is defined. It combines features of both prolog (for artificial intelligence) and autoview (for image processing). Predicates for image processing, controlling cameras, illumination sources, optics, a video multiplexor and simple robotic devices are all integrated with PROLOG2, an extension of standard core prolog. The result is a powerful medium for expressing a wide range of algorithms for the visual control of robots and advanced industrial inspection. Several provision applications (i.e. ‘programs’) are presented.     

Embedded system design with ada as the system design language

Recent research in software engineering has produced a number of techniques for structuring an understanding of systems. Many of these techniques are applicable to the design of embedded computer systems and produce designs whose structures are easily expressible in the ada language. This language is itself structured so that the design of a system can be expressed independently of its implementation. Thus ada can be a useful system design language (SDL) with these techniques. This paper describes the software design problem in the development of embedded computer systems. It shows how ada can be used as an SDL, as well as a system implementation language. The essential point is that as an SDL ada encourages designers to use recent theory to develop better structures for their systems, and its subsequent use to implement the systems preserves those structures in the product.     

Classifying sensor data with Calchas

Learning how to classify sensor data is one of the basic learning tasks in engineering. Data from sensors are usually made available over time, and are classified according to the behavior they exhibit in specific time intervals. This paper addresses the problem of classifying finite, univariate time series that are governed by unknown deterministic processes contaminated by noise. Time series in the same class are allowed to follow different processes. In this context, the appropriateness of using induction algorithms not specifically designed for temporal data is investigated. The paper presents Calchas, a simple supervised induction algorithm that uses serial correlation as its inductive bias in a Bayesian framework, and compares it empirically to a popular general-purpose classifier, in a NASA telemetry monitoring application. Two comparisons were performed: one in which the general purpose classifier was applied directly to the data, and another in which features that captured serial correlations were extracted before the induction. Serial correlation appeared to be an important form of inductive bias, most effectively utilized as an integral part of the learning algorithm. Feature extraction occurs too early in the training process to utilize correlation knowledge effectively.     

Citius altius fortius: Lessons learned from the Theorem Prover Waldmeister

In the last years, the development of automated theorem provers has been advancing in a so to speak Olympic spirit, following the motto “faster, higher, stronger”; and the Waldmeister system has been a part of that endeavour. We will survey the concepts underlying this prover, which implements Knuth-Bendix completion in its unfailing variant. The system architecture is based on a strict separation of active and passive facts, and is realized via specifically tailored representations for each of the central data structures: indexing for the active facts, set-based compression for the passive facts, successor sets for the conjectures. In order to cope with large search spaces, specialized redundancy criteria are employed, and the empirically gained control knowledge is integrated to ease the use of the system. We conclude with a discussion of strengths and weaknesses, and a view of future prospects.     

Subjective impressions of a non-naïve Unix and c beginner

This paper details an experienced programmer's first impressions of working with the Unix operating system and c programming language. Use of the Unix shell, vi editor, c compiler and some utilities are discussed, as are the Unix documentation and some relevant textbooks. An assessment of the difficulties and advantages of starting with Unix is given.     

A verified Common Lisp implementation of Buchberger’s algorithm in ACL2

In this article, we present the formal verification of a Common Lisp implementation of Buchberger’s algorithm for computing Gröbner bases of polynomial ideals. This work is carried out in ACL2, a system which provides an integrated environment where programming (in a pure functional subset of Common Lisp) and formal verification of programs, with the assistance of a theorem prover, are possible. Our implementation is written in a real programming language and it is directly executable within the ACL2 system or any compliant Common Lisp system. We provide here snippets of real verified code, discuss the formalization details in depth, and present quantitative data about the proof effort.     

Virtual Organizations in Arigatoni

Arigatoni is a lightweight overlay network that deploys the Global Computing Paradigm over the Internet. Communication for over the behavioral units of the overlay is performed by a simple resource discovery protocol (RDP). Basic Global Computers Units (GC) can communicate by first registering to a brokering service and then by mutually asking and offering services.Colonies and communities are the main entities in the model. A colony is a simple virtual organization composed by exactly one leader and some set (possibly empty) of individuals. A community is a raw set of colonies and global computers (think it as a soup of colonies and global computer without a leader).We present an operational semantics via a labeled transition system, that describes the main operations necessary in the Arigatoni model to perform leader negotiation, joining/leaving a colony, linking two colonies and moving one GC from one colony to another. Our formalization results to be adequate w.r.t. the algorithm performing peer logging/delogging and colony aggregation.     

A Breit–Pauli distorted wave implementation for autostructure

We describe the Breit–Pauli distorted wave (BPDW) approach for the electron-impact excitation of atomic ions that we have implemented within the autostructure code.

Program summary

Program title:autostructureCatalogue identifier: AEIV_v1_0Program summary URL:http://cpc.cs.qub.ac.uk/summaries/AEIV_v1_0.htmlProgram obtainable from: CPC Program Library, Queen?s University, Belfast, N. IrelandLicensing provisions: Standard CPC licence, http://cpc.cs.qub.ac.uk/licence/licence.htmlNo. of lines in distributed program, including test data, etc.: 130 987No. of bytes in distributed program, including test data, etc.: 1 031 584Distribution format: tar.gzProgramming language: Fortran 77/95Computer: GeneralOperating system: UnixHas the code been vectorized or parallelized?: Yes, a parallel version, with MPI directives, is included in the distribution.RAM: From several kbytes to several GbytesClassification: 2, 2.4Nature of problem: Collision strengths for the electron-impact excitation of atomic ions are calculated using a Breit–Pauli distorted wave approach with the optional inclusion of two-body non-fine-structure and fine-structure interactions.Solution method: General multi-configuration Breit–Pauli atomic structure. A jK-coupling partial wave expansion of the collision problem. Slater state angular algebra. Various model potential non-relativistic or kappa-averaged relativistic radial orbital solutions — the continuum distorted wave orbitals are not required to be orthogonal to the bound.Additional comments: Documentation is provided in the distribution file along with the test-case.Running time: From a few seconds to a few hours.     

A combinatorial algorithm for max csp

We consider the problem max csp over multi-valued domains with variables ranging over sets of size s_i?s and constraints involving k_j?k variables. We study two algorithms with approximation ratios A and B, respectively, so we obtain a solution with approximation ratio max(A,B).The first algorithm is based on the linear programming algorithm of Serna, Trevisan, and Xhafa [Proc. 15th Annual Symp. on Theoret. Aspects of Comput. Sci., 1998, pp. 488-498] and gives ratio A which is bounded below by s^1−k. For k=2, our bound in terms of the individual set sizes is the minimum over all constraints involving two variables of , where s₁ and s₂ are the set sizes for the two variables.We then give a simple combinatorial algorithm which has approximation ratio B, with B>A/e. The bound is greater than s^1−k/e in general, and greater than s^1−k(1−(s−1)/2(k−1)) for s?k−1, thus close to the s^1−k linear programming bound for large k. For k=2, the bound is if s=2, 1/2(s−1) if s?3, and in general greater than the minimum of 1/4s₁+1/4s₂ over constraints with set sizes s₁ and s₂, thus within a factor of two of the linear programming bound.For the case of k=2 and s=2 we prove an integrality gap of . This shows that our analysis is tight for any method that uses the linear programming upper bound.     

Kanga(ROO): Handling the micro-DST of the BaBar experiment with ROOT

A system based on ROOT for handling the micro-DST of the BaBar experiment is described. The purpose of the Kanga system is to have micro-DST data available in a format well suited for data distribution within a world-wide collaboration with many small sites. The design requirements, implementation and experience in practice after three years of data taking by the BaBar experiment are presented.