For the SL spec given below the type checker reports a warning saying Definition T1_f not used.. Since a trace definition is something you invoke from the command-line or combinatorial testing perspective I don't think the trace should ever be marked as 'unused'. One way to get rid of the warning is to export the definitions of the module. It is as if the type checker expects the trace to be invoked from within the module - like its a function or operation. If you do the equivalent PP model the trace does not get reported as unused.
module A
definitions
functions
f : () -> nat
f () == 1;
traces
T1_f:
f();
end A
PP version:
class A
functions
f : () -> nat
f () == 1;
traces
T1_f:
f();
end A
For the SL spec given below the type checker reports a warning saying
Definition T1_f not used.
. Since a trace definition is something you invoke from the command-line or combinatorial testing perspective I don't think the trace should ever be marked as 'unused'. One way to get rid of the warning is to export the definitions of the module. It is as if the type checker expects the trace to be invoked from within the module - like its a function or operation. If you do the equivalent PP model the trace does not get reported as unused.PP version: