Thu Jan 12 17:58:00 CET 2023

The original LOTOS specifications, which had been kept unchanged since 1997,
have been simplified by removing many LOTOS operations that were defined
but not used:

    First, Last: -> Atom
    Succ, Pred: Atom -> Atom
    is_white, is_black, is_square: Atom -> Bool
    _NotIn_: Atom, Knowledge -> Bool
    _Union_, _Ints_, _Minus_: Knowledge, Knowledge -> Knowledge
    _eq_, _ne_, _Includes_, _IsSubsetOf_: Knowledge, Knowledge -> Bool
    Card: Knowledge -> Nat
    Is_assert: Change -> Bool
    Is_retract: Change -> Bool
    String: Change -> Proposal
    _++_ : Proposal, Proposal -> Proposal (* identical to operation _*_ *)
    Reverse: Proposal -> Proposal
    Length: Proposal -> Nat
    First, Last: -> UserAction
    Succ, Pred: UserAction -> UserAction
    is_doregister, is_doevaluate, is_doachieve, is_doforward, is_dodeny,
       is_doaccept, is_doreject, is_dochallenge: UserAction -> Bool
    First, Last: -> SignalVal
    Succ, Pred: SignalVal -> SignalVal
    is_sigregistered, is_sigstored, is_signotinA, is_signotinP, is_signotinC,
       is_signotconsistent: SignalVal -> Bool
    Set_id: Id, SubmittedEntry -> SubmittedEntry
    Set_req: Request, SubmittedEntry -> SubmittedEntry
    _Over_: SubmittedTbl, SubmittedTbl -> SubmittedTbl
    _IsSubTableOf_: SubmittedTbl, SubmittedTbl -> Bool
    Test: SubmittedEntry, SubmittedTbl -> Bool
    _eq_, _ne_, _Includes_: SubmittedTbl, SubmittedTbl -> Bool
    Card: SubmittedTbl -> Nat
    Set_id: Id, GrpSubmittedEntry -> GrpSubmittedEntry
    Set_req: Request, GrpSubmittedEntry -> GrpSubmittedEntry
    Set_sender: BaseId, GrpSubmittedEntry -> GrpSubmittedEntry
    Set_senderid: Id, GrpSubmittedEntry -> GrpSubmittedEntry
    _ne_: GrpSubmittedEntry, GrpSubmittedEntry -> Bool
    Test: GrpSubmittedEntry, GrpSubmittedTbl -> Bool
    _Over_: GrpSubmittedTbl, GrpSubmittedTbl -> GrpSubmittedTbl
    _eq_, _ne_, _Includes_: GrpSubmittedTbl, GrpSubmittedTbl -> Bool
    _IsSubTableOf_: GrpSubmittedTbl, GrpSubmittedTbl -> Bool
    Card: GrpSubmittedTbl -> Nat
    First, Last: -> Status
    Succ, Pred: Status -> Status
    is_new, is_accepted, is_rejected, is_challenged: Status -> Bool
    Set_id: Id, PendingEntry -> PendingEntry
    Set_req: Request, PendingEntry -> PendingEntry
    Test: PendingEntry, PendingTbl -> Bool
    _Over_: PendingTbl, PendingTbl -> PendingTbl
    _eq_, _ne_, _Includes_: PendingTbl, PendingTbl -> Bool
    _IsSubTableOf_: PendingTbl, PendingTbl -> Bool
    Card: PendingTbl -> Nat
    searchproposal: Proposal, PendingTbl -> Bool
    getproposal: Proposal, PendingTbl -> PendingEntry
    _NotIn_: BaseId, SubscriberSet -> Bool
    _Union_, _Ints_, _Minus_: SubscriberSet, SubscriberSet -> SubscriberSet
    _IsSubsetOf_: SubscriberSet, SubscriberSet -> Bool
    Set_id: Id, CfcEntry -> CfcEntry
    Set_sender: BaseId, CfcEntry -> CfcEntry
    Set_senderid: Id, CfcEntry -> CfcEntry
    Set_req: Request, CfcEntry -> CfcEntry
    _Over_: CfcTbl, CfcTbl -> CfcTbl
    _IsSubTableOf_: CfcTbl, CfcTbl -> Bool
    Card: CfcTbl -> Nat
    _OrElse_: ParentBase, BaseId -> BaseId
    Set_sender: BaseId, Packet -> Packet
    Set_receiver: BaseId, Packet -> Packet
    Set_message: Message, Packet -> Packet
    String: Packet -> PacketQueue
    _+_: Packet, Packet -> PacketQueue
    _++_: PacketQueue, PacketQueue -> PacketQueue
    Reverse: PacketQueue -> PacketQueue
    Length: PacketQueue -> Nat
    Last: PacketQueue -> Packet
    ButLast: PacketQueue -> PacketQueue
    nth: PacketQueue, Nat -> Packet
    SubStr: PacketQueue, Nat, Nat -> PacketQueue
    Remove: Packet, PacketQueue -> PacketQueue
    _IsIn_, _NotIn_: Packet, PacketQueue -> Bool
    _Includes_, _IsSubStrOf_: PacketQueue, PacketQueue -> Bool

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

Mon Oct 30 10:52:59 CET 2023

Further changes have been brought by Hubert Garavel, especially to ensure
compatibility between the LOTOS and LNT specifications of the CO4 system.

In CO4_DATATYPES.lib:

   - Removal of the operations base7, base8, base9:-> BaseId because they
     were unused.

   - Addition of an operation _lt_ for the type BaseId.

   - Addition of a special comment (*! list *) to the sort Proposal, to
     ensure that the values of this sort are displayed identically in both
     the LOTOS and LNT specifications.

   - Modification of the pick: SubscriberSet -> BaseId operation, which no
     longer returns the first element of a SubscriberSet, but the smallest
     element (since, in LNT, set elements are sorted by increasing order).

In CO4_PROCESSES.lib:

   - Renaming of get in Get, to match the name declared in CO4_DATATYPES.lib.

   - Renaming of is_reqachieve, is_notify, etc. to Is_reqachieve, Is_notify,
     etc. to ensure that these operations are called with the same name as
     they have been declared.

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

Execution using Make (obsolete)
===============================

In the LOTOS sub-directory, you can also call Make with an appropriate
target. The available targets are

$ make -f makefile.old

  Note: The whole execution of the makefile is quite long (about 1 hour
	50 minutes on an Ultra-1 using CADP version 97b "Liege").

  To compile and perform all verifications for a single variant, e.g.
  "co4_3_1.lotos", type

$ make -f makefile.old co4_3_1.result

  The results are logged into a file "co4_3_1.result".

  You can also execute all compilations and verifications by typing

$ make -f makefile.old results

  but be warned that this starts some very long and greedy
  computations that could exhaust the memory space of your
  computer. We have achieved a successful run of the whole set in 256
  MB RAM plus 150 MB swap space.

  Two transition graphs can also be pretty-printed using BCG_DRAW by
  typing

$ make -f makefile.old draws

  and then displaying or printing the produced PostScript files.

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