Bug 195 - Add scalar sets
Summary: Add scalar sets
Status: RESOLVED FIXED
Alias: None
Product: UPPAAL
Classification: Unclassified
Component: Engine (show other bugs)
Version: unspecified
Hardware: All All
: P1 enhancement
Assignee: Gerd Behrmann
URL:
Depends on:
Blocks: 196
  Show dependency treegraph
 
Reported: 2005-09-03 20:43 CEST by Gerd Behrmann
Modified: 2005-11-09 12:44 CET (History)
1 user (show)

See Also:
Architecture:


Attachments

Note You need to log in before you can comment on or make changes to this bug.
Description Gerd Behrmann 2005-09-03 20:43:31 CEST
In order to implement symmetry reduction, we need to add scalarsets to the language. A scalarset is a 
type similar to integers, but with a severely restricted set of operations.

Scalarsets are constructed using the type expression

  scalar[n]

where n is the size of the scalar set (this is not unlike the syntax for defining bounded integers). This is 
not to be confused with array declarations.

The only valid operations on scalars (the elements of scalarsets) are equallity ==, inequallity != and 
assignment =.  Scalars use name equivalence, i.e., both arguments must belong to the *same* 
scalarset. E.g.

  scalar[2] a; scalar[2] b; a = b;

fails as a and b belong to two different scalars sets. The correct thing would be

  scalar[2] a, b; a = b;

or

  typename scalar[2] myset_t; myset_t a; myset_t b; a = b;


It must be possible to declare arrays or templatesets over scalars, e.g.

  typedef scalar[2] myset_t;
  int a[myset_t];
  process P[i:myset_t]() { ... }


Constant scalars are hard to support with symmetry reduction (it is possible, but the constant scalar 
would need to be stored in the state vector thus reducing the usefulness of declaring it as a constant). 
For the same reason it is not allowed to compare scalars to integer literals. 

Initialisers for scalars, however, should be supported, e.g.
 
  myset a = 1;

but not for function local variables, as this would again complicate symmetry reduction.
Comment 1 Gerd Behrmann 2005-09-03 21:01:57 CEST
I forgot to mention that 

- iterators 
- the forall quantifier 
- the select feature on edges

must work with scalarsets.
Comment 2 Gerd Behrmann 2005-11-06 17:45:38 CET
Part of this has been implemented. Increasing priority, as we should have this in for 3.6 alpha 2.
Comment 3 Gerd Behrmann 2005-11-09 12:44:21 CET
Implemented in CVS.