% TESTED FEATURES: while, select
% EXPECTED OUTCOME: Unsafe
specification Loop_Unsafe
channel_model CCM
entity Loop
{
    symbols
        f1, f2, f3 : fact;
        tok1, tok2, tok3 : message;
    body
    {
        f1;
        f2;
        f3;
        while (true)
        {
            select
            {
                on (f1) :
                {
                    iknows(tok1);
                }
                on (f2) :
                {
                    iknows(tok2);
                }
                on (f3) :
                {
                    iknows(tok3);
                }				
            }
        }
    }
    goals
        Finish : 
          [](!(exists D . 
               (iknows(tok1) 
              & iknows(tok2) 
              & iknows(tok3))
             ));
}