------------------------------ MODULE serie6_1 ------------------------------
EXTENDS Naturals, Integers, TLC, Reals
CONSTANTS a0, b0, c0

=============================================================================
\* Modification History
\* Last modified Mon Nov 23 11:14:29 CET 2015 by arthur
\* Created Mon Nov 23 10:18:52 CET 2015 by arthur

(*
--algorithm resolution {
variables a=a0, b=b0, c=b0, determinant;
{
  l0:determinant:=b*b-4*a*c;
  if (determinant>0)
  {
      print <<"Roots are:">>;
  }
  else if (determinant==0)
  {
    print <<"Roots are: ">>;
  }
  else
  {
    real:= -b/(2*a);
    imag := sqrt(-determinant)/(2*a);
    print <<"Roots are: %.2f+%.2fi and %.2f-%.2fi", real, imag, real, imag>>;
  }
}
}
*)
\* BEGIN TRANSLATION
CONSTANT defaultInitValue
VARIABLES a, b, c, determinant, pc

vars == << a, b, c, determinant, pc >>

Init == (* Global variables *)
        /\ a = a0
        /\ b = b0
        /\ c = b0
        /\ determinant = defaultInitValue
        /\ pc = "l0"

l0 == /\ pc = "l0"
      /\ determinant' = b*b-4*a*c
      /\ IF determinant'>0
            THEN /\ PrintT(<<"Roots are:">>)
            ELSE /\ IF determinant'==0
                       THEN /\ PrintT(<<"Roots are: ">>)
                       ELSE /\ real' = -b/(2*a)
                            /\ imag' = sqrt(-determinant')/(2*a)
                            /\ PrintT(<<"Roots are: %.2f+%.2fi and %.2f-%.2fi", real, imag, real, imag>>)
      /\ pc' = "Done"
      /\ UNCHANGED << a, b, c >>

Next == l0
           \/ (* Disjunct to prevent deadlock on termination *)
              (pc = "Done" /\ UNCHANGED vars)

Spec == Init /\ [][Next]_vars

Termination == <>(pc = "Done")

\* END TRANSLATION