*** In the repair service part of the protocol, there is a use case *** leading to "error". The following module defines some *** possible ERROR constructors which can be used. *** Note that ERROR-objects are not of sort Object, so that *** the tick rule in module DETERMINISTIC-TICK-RULE does not *** apply on a state which contains an error element. (tomod ERROR-OBJECT is protecting STRING . op ERROR : String -> Configuration [format (nr c)] . op ERROR : String Configuration -> Configuration [format (nr c)] . op ERROR : String AttributeSet -> Configuration [format (nr c)] . op ERROR : String Oid Cid AttributeSet -> Configuration [format (nr c)] . endtom)