|
32 | 32 | FalseFormula, |
33 | 33 | Formula, |
34 | 34 | Implies, |
| 35 | + Logic, |
35 | 36 | Not, |
36 | 37 | Or, |
37 | 38 | TrueFormula, |
38 | 39 | ) |
39 | | -from pylogics.syntax.ldl import ( |
40 | | - Box, |
41 | | - Diamond, |
42 | | - LDLFalse, |
43 | | - LDLTrue, |
44 | | - Prop, |
45 | | - Seq, |
46 | | - Star, |
47 | | - Test, |
48 | | - Union, |
49 | | -) |
| 40 | +from pylogics.syntax.ldl import Box, Diamond, Prop, Seq, Star, Test, Union |
50 | 41 | from pylogics.syntax.ltl import ( |
51 | 42 | Always, |
52 | 43 | Eventually, |
@@ -111,28 +102,16 @@ def to_string_atomic(formula: AbstractAtomic) -> str: |
111 | 102 | return formula.name |
112 | 103 |
|
113 | 104 |
|
114 | | -@to_string.register(TrueFormula) |
115 | | -def to_string_true(_formula: TrueFormula) -> str: |
116 | | - """Transform the "true" formula into string.""" |
117 | | - return "true" |
118 | | - |
119 | | - |
120 | | -@to_string.register(FalseFormula) |
121 | | -def to_string_false(_formula: FalseFormula) -> str: |
122 | | - """Transform the "false" formula into string.""" |
123 | | - return "false" |
124 | | - |
125 | | - |
126 | 105 | @to_string.register(Next) |
127 | 106 | def to_string_next(formula: Next) -> str: |
128 | 107 | """Transform a next formula into string.""" |
129 | | - return f"X({to_string(formula.argument)})" |
| 108 | + return f"X[!]({to_string(formula.argument)})" |
130 | 109 |
|
131 | 110 |
|
132 | 111 | @to_string.register(WeakNext) |
133 | 112 | def to_string_weak_next(formula: WeakNext): |
134 | 113 | """Transform the weak next formula.""" |
135 | | - return f"W({to_string(formula.argument)})" |
| 114 | + return f"X({to_string(formula.argument)})" |
136 | 115 |
|
137 | 116 |
|
138 | 117 | @to_string.register(Until) |
@@ -208,16 +187,16 @@ def to_string_pltl_historically(formula: Historically) -> str: |
208 | 187 | return f"H({to_string(formula.argument)})" |
209 | 188 |
|
210 | 189 |
|
211 | | -@to_string.register(LDLTrue) |
212 | | -def to_string_ldl_true(_formula: LDLTrue) -> str: |
213 | | - """Transform an LDL true into string.""" |
214 | | - return "tt" |
| 190 | +@to_string.register(TrueFormula) |
| 191 | +def to_string_ldl_true(formula: TrueFormula) -> str: |
| 192 | + """Transform a true into string.""" |
| 193 | + return "tt" if formula.logic != Logic.PL else "true" |
215 | 194 |
|
216 | 195 |
|
217 | | -@to_string.register(LDLFalse) |
218 | | -def to_string_ldl_false(_formula: LDLFalse) -> str: |
219 | | - """Transform an LDL false into string.""" |
220 | | - return "ff" |
| 196 | +@to_string.register(FalseFormula) |
| 197 | +def to_string_ldl_false(formula: FalseFormula) -> str: |
| 198 | + """Transform a false into string.""" |
| 199 | + return "ff" if formula.logic != Logic.PL else "false" |
221 | 200 |
|
222 | 201 |
|
223 | 202 | @to_string.register(Diamond) |
|
0 commit comments