Adding support for labels inside labels

[maxkurze1]

Fix issue #178

• allows labels to be placed inside other labels. This can look like: label "l1" = "l2" & "l3";
• adds check to find cyclic dependencies between labels (also finds cycles between labels and formulas if formulas are expanded before running the check)
• changing label evaluation to evaluate all labels together instead of one by one
• by allowing labels inside other label-definitions labels are also allowed inside guards, therefore also adding support for label evaluation inside guards

Example:

dtmc

module test
	s : [0..3] init 0;
        d : [0..1] init 0;

	[] s=0 -> 0.1 : (s'=1) + 0.3 : (s'=2) + 0.6 : (s'=3);
	[] s=1 -> (s'=1);
	[] s=2 -> (s'=2) & (d'=1);
	[] s=3 -> (s'=3) & (d'=1);
endmodule

// true for s=2 or 3
label "l1" = d=1;
// true for s=2
label "l2" = s=2;
// true for s=0 or 2
label "l3" = ("l1" & "l2") | s=0;

// true for s=0 or 2 or 3
formula f1 = "l1" | s=0;
// true for s=0 or 2
label "l4" = "l3" & f1

Also module renaming doesn't affect the evaluation of the label. The label used inside the guard stays the same.

dtmc

module m1
    s1: bool init false;

    [] !"foo" -> (s1'=true);
    [] true -> (s1'=false);
endmodule

module m2=m1[s1=s2] endmodule

label "foo" = s1 | s2;