File tree Expand file tree Collapse file tree 2 files changed +98
-0
lines changed
liquidjava-example/src/main/java/testSuite Expand file tree Collapse file tree 2 files changed +98
-0
lines changed Original file line number Diff line number Diff line change 1+ package testSuite ;
2+
3+ import liquidjava .specification .Refinement ;
4+ import liquidjava .specification .StateRefinement ;
5+ import liquidjava .specification .StateSet ;
6+ @ StateSet ({"green" , "amber" , "red" })
7+ public class CorrectTrafficLightRGB {
8+
9+ @ Refinement ("r >= 0 && r <= 255" ) int r ;
10+
11+ @ Refinement ("g >= 0 && g <= 255" ) int g ;
12+
13+ @ Refinement ("b >= 0 && b <= 255" ) int b ;
14+
15+ @ StateRefinement (to = "green(this)" )
16+ public CorrectTrafficLightRGB () {
17+ r = 255 ;
18+ g = 0 ;
19+ b = 0 ;
20+ }
21+
22+ @ StateRefinement (from = "green(this)" , to = "amber(this)" )
23+ public void transitionToAmber () {
24+ r = 255 ;
25+ g = 120 ;
26+ b = 0 ;
27+ }
28+
29+ @ StateRefinement (from = "red(this)" , to = "green(this)" )
30+ public void transitionToGreen () {
31+ r = 76 ;
32+ g = 187 ;
33+ b = 23 ;
34+ }
35+
36+ @ StateRefinement (from = "amber(this)" , to = "red(this)" )
37+ public void transitionToRed () {
38+ r = 230 ;
39+ g = 0 ;
40+ b = 1 ;
41+ }
42+
43+
44+ public static void name () {
45+ CorrectTrafficLightRGB tl = new CorrectTrafficLightRGB ();
46+ tl .transitionToAmber ();
47+ tl .transitionToRed ();
48+ }
49+ }
Original file line number Diff line number Diff line change 1+ package testSuite ;
2+
3+ import liquidjava .specification .Refinement ;
4+ import liquidjava .specification .StateRefinement ;
5+ import liquidjava .specification .StateSet ;
6+ @ StateSet ({"green" , "amber" , "red" })
7+ public class ErrorTrafficLightRGB {
8+
9+ @ Refinement ("r >= 0 && r <= 255" ) int r ;
10+
11+ @ Refinement ("g >= 0 && g <= 255" ) int g ;
12+
13+ @ Refinement ("b >= 0 && b <= 255" ) int b ;
14+
15+ @ StateRefinement (to = "green(this)" )
16+ public ErrorTrafficLightRGB () {
17+ r = 255 ;
18+ g = 0 ;
19+ b = 0 ;
20+ }
21+
22+ @ StateRefinement (from = "green(this)" , to = "amber(this)" )
23+ public void transitionToAmber () {
24+ r = 255 ;
25+ g = 120 ;
26+ b = 0 ;
27+ }
28+
29+ @ StateRefinement (from = "red(this)" , to = "green(this)" )
30+ public void transitionToGreen () {
31+ r = 76 ;
32+ g = 187 ;
33+ b = 23 ;
34+ }
35+
36+ @ StateRefinement (from = "amber(this)" , to = "red(this)" )
37+ public void transitionToRed () {
38+ r = 230 ;
39+ g = 0 ;
40+ b = 1 ;
41+ }
42+
43+
44+ public static void name () {
45+ ErrorTrafficLightRGB tl = new ErrorTrafficLightRGB ();
46+ tl .transitionToAmber ();
47+ tl .transitionToRed ();
48+ }
49+ }
You can’t perform that action at this time.
0 commit comments