search

GLaDOS-Michigan / dafnyMC

Integrating protocol debugging workflows into dafny
https://dafny-lang.github.io/dafny/
Other
0 stars 0 forks source link

Cardinality of Sequences #3

Closed TonyZhangND closed 2 years ago

TonyZhangND commented 2 years ago

Consider a record type definition

Variables == [type : {"Variables"}, server : ServerGrant, clients : [1..5 -> ClientRecord]]

and the expression Cardinality(v.clients). Evaluating this expression leads to the error

Error: Attempted to compute cardinality of the value
<< [type |-> "Released"],
   [type |-> "Released"],
   [type |-> "Released"],
   [type |-> "Released"],
   [type |-> "Released"] >>

It looks like TLC cannot evaluate the cardinality of sequences, i.e. relations. For instance, Cardinality(<<1,2,3>>) results in the same error.

To evaluate cardinality of relations in general, we need to use the expression

`Cardinality(DOMAIN(<<1,2,3>>))`
TonyZhangND commented 2 years ago

fixed in c3af6294dff01611ea2b7b2cebe5f52a70829fd5