Mon Mar 23 16:34:40 CET 2015

Frederic Lang and Hubert Garavel simplified the LOTOS specification of the
CFS by deleting 155 lines of LOTOS code.

The following processes have been deleted since they were not used:

    ChannelProxy12
    ChannelProxy21
    Master1with2
    OutputCell12
    OutputCell123
    OutputCell1with2
    OutputCell2with1
    Proxy12
    Proxy21
    Site1
    Site12
    Site123
    Site1with2
    Site2with1
    Site1with23
    Site2Proxy

These three processes have been merged into a single parameterized process 
GeneralUser:

    GeneralUser1
    GeneralUser2
    GeneralUser3

The following processes have been expanded inline directly into the SVL script
and removed:

    ChannelProxy123
    ChannelProxy213,
    ChannelProxy312
    Master1
    OutputCell1
    OutputCell2
    OutputCell3
    Proxy123
    Proxy213
    Proxy312
    Site2
    Site3

-------------------------------------------------------------------------------

Thu Nov  2 16:07:43 CET 2023

Hubert Garavel further simplified the LOTOS specification of the CFS by
removing many LOTOS operations that were defined but not used:

    First, Last: -> Site
    Succ, Pred: Site -> Site
    is_site1, is_site2, is_site3: Site -> Bool 
    First, Last: -> Val
    Succ, Pred: Val -> Val
    is_val1, is_val2: Val -> Bool 
    First, Last: -> CfsCall
    Succ, Pred: CfsCall -> CfsCall
    is_read, is_beginwrite, is_endwrite: CfsCall -> Bool 
    First, Last: -> Message
    is_readrq, is_readok, is_writerq, is_writeok: Message -> Bool 
    is_invalidate, is_firstmaster: Message -> Bool 
    Succ, Pred: Message -> Message
    First, Last: -> State
    Succ, Pred: State -> State
    is_master, is_writing, is_invalid, is_valid, is_waitread: State -> Bool
    is_waitwrite, is_flushrqs, is_forwardrqs, is_invalwriting: State -> Bool
    is_invalinvalid: State -> Bool 
    istransient: State -> Bool
    ismaster: State -> Bool
    {*}: -> SiteSet
    max: SiteSet -> Site
    butmax: SiteSet -> SiteSet
    _isin_, _notin_: Site, SiteSet -> Bool
    _union_, _ints_, _minus_: SiteSet, SiteSet -> SiteSet
    _includes_, _issubsetof_: SiteSet, SiteSet -> Bool
    card: SiteSet -> Nat
    Set_site: Site, Pkt -> Pkt
    Set_msg: Message, Pkt -> Pkt
    String: Pkt -> PktList
    _+_: Pkt, Pkt -> PktList
    _++_: PktList, PktList -> PktList
    Reverse: PktList -> PktList
    Length: PktList -> Nat
    Last: PktList -> Pkt
    ButLast: PktList -> PktList
    nth: PktList, Nat -> Pkt
    SubStr: PktList, Nat, Nat -> PktList
    Remove: Pkt, PktList -> PktList
    _IsIn_, _NotIn_: Pkt, PktList -> Bool
    _IsPrefixOf_, _IsSuffixOf_: PktList, PktList -> Bool
    _Includes_, _IsSubStrOf_: PktList, PktList -> Bool
    _eq_, _ne_: ValArray, ValArray -> Bool 

Other operations have been expanded in-line and removed:
    fill: Val -> ValArray
    init: -> Val

The following process has been removed since it was useless:
    Channel2Proxy

-------------------------------------------------------------------------------