Equivalent
- ¬ (F p → ¬ p U (p ∧ ¬ q W q W ¬ q W q W G ¬ q))
- F p ∧ (¬ p ∨ (((F q U (¬ q ∧ F q)) U (q ∧ F q U (¬ q ∧ F q))) U (¬ q ∧ (F q U (¬ q ∧ F q)) U (q ∧ F q U (¬ q ∧ F q)))) U (q ∧ ((F q U (¬ q ∧ F q)) U (q ∧ F q U (¬ q ∧ F q))) U (¬ q ∧ (F q U (¬ q ∧ F q)) U (q ∧ F q U (¬ q ∧ F q))))) W (p ∧ (¬ p ∨ (((F q U (¬ q ∧ F q)) U (q ∧ F q U (¬ q ∧ F q))) U (¬ q ∧ (F q U (¬ q ∧ F q)) U (q ∧ F q U (¬ q ∧ F q)))) U (q ∧ ((F q U (¬ q ∧ F q)) U (q ∧ F q U (¬ q ∧ F q))) U (¬ q ∧ (F q U (¬ q ∧ F q)) U (q ∧ F q U (¬ q ∧ F q))))))
Complement
Classification
| Temporal Hierarchy |
|---|
| Unknown |
| Spec Patterns |
|---|
| Unknown |
| DBW-Recognizable |
|---|
| Unknown |
| Automaton Type: Nondeterministic Büchi | |||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|
| #1 | ID: 745 | Author: Ming-Hsien Tsai | #2 | ID: 2978 | Author: GOAL | #3 | ID: 646 | Author: GOAL | |||
| St: 7 | Tr: 28 | Date: 2011-08-23 00:00:00 | St: 8 | Tr: 32 | Date: 2012-05-24 08:31:35 | St: 46 | Tr: 233 | Date: 2010-01-19 00:00:00 | |||
| Description: | Description: | Description: | |||||||||
| Download: GFF Promela Add to Cart | Download: GFF Promela Add to Cart | Download: GFF Promela Add to Cart | |||||||||
|
Acceptance condition: {s8} |
Acceptance condition: s3, s5 |
Acceptance condition: {s4, s6, s8, s14, s21, s28} |
|||||||||
|
|
|
|||||||||
| Automaton Type: Deterministic Büchi | |||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|
| #1 | ID: 2568 | Author: GOAL | #2 | ID: 2978 | Author: GOAL | #3 | ID: 2500 | Author: GOAL | |||
| St: 8 | Tr: 32 | Date: 2011-12-07 00:00:00 | St: 8 | Tr: 32 | Date: 2012-05-24 08:31:35 | St: 10 | Tr: 40 | Date: 2011-12-07 00:00:00 | |||
| Description: | Description: | Description: | |||||||||
| Download: GFF Promela Add to Cart | Download: GFF Promela Add to Cart | Download: GFF Promela Add to Cart | |||||||||
|
Acceptance condition: {s0, s7} |
Acceptance condition: s3, s5 |
Acceptance condition: {s0, s4, s5, s9} |
|||||||||
|
|
|
|||||||||
| Automaton Type: Nondeterministic Co-Büchi | |||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|
| #1 | ID: 2339 | Author: GOAL | #2 | ID: 2305 | Author: GOAL | #3 | N/A | ||||
| St: 7 | Tr: 28 | Date: 2011-12-07 00:00:00 | St: 337 | Tr: 1348 | Date: 2011-12-07 00:00:00 | ||||||
| Description: | Description: | ||||||||||
| Download: GFF Add to Cart | Download: GFF Add to Cart | ||||||||||
|
Acceptance condition: {s0, s1, s2, s3, s4, s5} |
Acceptance condition: {s0, s2, s6, s8, s10, s11, s12, s13, s14, s15, s17, s19, s23, s27, s30, s31, s32, s33, s35, s37, s38, s39, s42, s43, s51, s67, s69, s72, s73, s76, s81, s82, s83, s84, s91, s92, s98, s99, s100, s103, s112, s113, s114, s120, s123, s125, s130, s132, s144, s145, s146, s148, s149, s151, s158, s159, s160, s162, s163, s164, s165, s166, s171, s174, s176, s199, s203, s205, s211, s214, s215, s219, s221, s224, s225, s227, s228, s229, s230, s231, s235, s236, s237, s289, s291, s293, s295, s296, s298, s307, s309, s312, s313, s314, s319, s321, s322, s325, s326, s330} |
||||||||||
|
|
||||||||||
| Automaton Type: Deterministic Co-Büchi | |||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|
| #1 | ID: 2339 | Author: GOAL | #2 | ID: 2305 | Author: GOAL | #3 | N/A | ||||
| St: 7 | Tr: 28 | Date: 2011-12-07 00:00:00 | St: 337 | Tr: 1348 | Date: 2011-12-07 00:00:00 | ||||||
| Description: | Description: | ||||||||||
| Download: GFF Add to Cart | Download: GFF Add to Cart | ||||||||||
|
Acceptance condition: {s0, s1, s2, s3, s4, s5} |
Acceptance condition: {s0, s2, s6, s8, s10, s11, s12, s13, s14, s15, s17, s19, s23, s27, s30, s31, s32, s33, s35, s37, s38, s39, s42, s43, s51, s67, s69, s72, s73, s76, s81, s82, s83, s84, s91, s92, s98, s99, s100, s103, s112, s113, s114, s120, s123, s125, s130, s132, s144, s145, s146, s148, s149, s151, s158, s159, s160, s162, s163, s164, s165, s166, s171, s174, s176, s199, s203, s205, s211, s214, s215, s219, s221, s224, s225, s227, s228, s229, s230, s231, s235, s236, s237, s289, s291, s293, s295, s296, s298, s307, s309, s312, s313, s314, s319, s321, s322, s325, s326, s330} |
||||||||||
|
|
|
||||||||||
| Automaton Type: Nondeterministic Muller | |||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|
| #1 | ID: 1067 | Author: GOAL | #2 | N/A | #3 | N/A | |||||
| St: 7 | Tr: 28 | Date: 2011-12-07 00:00:00 | |||||||||
| Description: | |||||||||||
| Download: GFF Add to Cart | |||||||||||
|
Acceptance condition: { {s8} } |
|||||||||||
|
|||||||||||
| Automaton Type: Nondeterministic Rabin | |||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|
| #1 | ID: 1392 | Author: GOAL | #2 | ID: 1337 | Author: GOAL | #3 | ID: 1331 | Author: GOAL | |||
| St: 7 | Tr: 28 | Date: 2011-12-07 00:00:00 | St: 46 | Tr: 233 | Date: 2011-12-07 00:00:00 | St: 61 | Tr: 312 | Date: 2011-12-07 00:00:00 | |||
| Description: | Description: | Description: | |||||||||
| Download: GFF Add to Cart | Download: GFF Add to Cart | Download: GFF Add to Cart | |||||||||
|
Acceptance condition: { (∅, {s8}) } |
Acceptance condition: { (∅, {s4, s6, s8, s14, s21, s28}) } |
Acceptance condition: { (∅, {s3, s7, s9, s12, s18, s23, s26, s28, s29, s33, s43, s45, s51}) } |
|||||||||
|
|
|
|||||||||
| Automaton Type: Nondeterministic Streett | |||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|
| #1 | ID: 1717 | Author: GOAL | #2 | ID: 1662 | Author: GOAL | #3 | ID: 1656 | Author: GOAL | |||
| St: 7 | Tr: 28 | Date: 2011-12-07 00:00:00 | St: 46 | Tr: 233 | Date: 2011-12-07 00:00:00 | St: 61 | Tr: 312 | Date: 2011-12-07 00:00:00 | |||
| Description: | Description: | Description: | |||||||||
| Download: GFF Add to Cart | Download: GFF Add to Cart | Download: GFF Add to Cart | |||||||||
|
Acceptance condition: { ({s8}, {s0, s1, s2, s3, s5, s6, s8}) } |
Acceptance condition: { ({s4, s6, s8, s14, s21, s28}, {s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, s17, s18, s19, s20, s21, s22, s23, s24, s25, s26, s27, s28, s29, s30, s31, s32, s33, s34, s35, s36, s37, s38, s39, s40, s41, s42, s43, s44, s45}) } |
Acceptance condition: { ({s3, s7, s9, s12, s18, s23, s26, s28, s29, s33, s43, s45, s51}, {s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, s17, s18, s19, s20, s21, s22, s23, s24, s25, s26, s27, s28, s29, s30, s31, s32, s33, s34, s35, s36, s37, s38, s39, s40, s41, s42, s43, s44, s45, s46, s47, s48, s49, s50, s51, s52, s53, s54, s55, s56, s57, s58, s59, s60}) } |
|||||||||
|
|
|
|||||||||
| Automaton Type: Nondeterministic Parity | |||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|
| #1 | ID: 2042 | Author: GOAL | #2 | ID: 1987 | Author: GOAL | #3 | ID: 1981 | Author: GOAL | |||
| St: 7 | Tr: 28 | Date: 2011-12-07 00:00:00 | St: 46 | Tr: 233 | Date: 2011-12-07 00:00:00 | St: 61 | Tr: 312 | Date: 2011-12-07 00:00:00 | |||
| Description: | Description: | Description: | |||||||||
| Download: GFF Add to Cart | Download: GFF Add to Cart | Download: GFF Add to Cart | |||||||||
|
Acceptance condition: 0: {s8}, 1: {s0, s1, s2, s3, s5, s6} |
Acceptance condition: 0: {s4, s6, s8, s14, s21, s28}, 1: {s0, s1, s2, s3, s5, s7, s9, s10, s11, s12, s13, s15, s16, s17, s18, s19, s20, s22, s23, s24, s25, s26, s27, s29, s30, s31, s32, s33, s34, s35, s36, s37, s38, s39, s40, s41, s42, s43, s44, s45} |
Acceptance condition: 0: {s3, s7, s9, s12, s18, s23, s26, s28, s29, s33, s43, s45, s51}, 1: {s0, s1, s2, s4, s5, s6, s8, s10, s11, s13, s14, s15, s16, s17, s19, s20, s21, s22, s24, s25, s27, s30, s31, s32, s34, s35, s36, s37, s38, s39, s40, s41, s42, s44, s46, s47, s48, s49, s50, s52, s53, s54, s55, s56, s57, s58, s59, s60} |
|||||||||
|
|
|
|||||||||
| Automaton Type: Deterministic Parity | |||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|
| #1 | ID: 2884 | Author: GOAL | #2 | ID: 2837 | Author: GOAL | #3 | N/A | ||||
| St: 8 | Tr: 32 | Date: 2011-12-07 00:00:00 | St: 781 | Tr: 3124 | Date: 2011-12-07 00:00:00 | ||||||
| Description: | Description: | ||||||||||
| Download: GFF Add to Cart | Download: GFF Add to Cart | ||||||||||
|
Acceptance condition: 0: {s0, s7}, 1: {s1, s2, s3, s4, s5, s6} |
Acceptance condition: 0: {s0, s27, s29, s368, s370, s372, s377, s380, s381, s395, s396, s447, s452, s455}, 2: {s24, s28, s33, s38, s47, s49, s54, s56, s64, s66, s71, s86, s90, s93, s95, s98, s100, s104, s105, s112, s113, s121, s128, s129, s133, s143, s145, s146, s148, s150, s153, s155, s157, s158, s159, s160, s161, s162, s163, s164, s165, s166, s167, s168, s169, s170, s171, s172, s173, s174, s175, s176, s178, s180, s182, s184, s186, s187, s189, s191, s193, s194, s195, s196, s198, s200, s201, s202, s203, s204, s205, s211, s213, s214, s216, s218, s219, s220, s221, s222, s223, s225, s229, s230, s231, s232, s235, s237, s238, s240, s242, s243, s244, s246, s248, s250, s251, s252, s253, s254, s255, s256, s257, s258, s259, s260, s261, s262, s263, s264, s265, s266, s267, s269, s271, s272, s273, s275, s278, s281, s283, s284, s286, s288, s289, s290, s291, s292, s294, s298, s299, s300, s301, s303, s305, s311, s313, s314, s316, s318, s319, s320, s321, s322, s323, s324, s326, s330, s331, s332, s358, s360, s362, s365, s366, s367, s369, s371, s375, s376, s379, s386, s387, s388, s389, s390, s391, s392, s393, s394, s397, s398, s402, s403, s404, s405, s406, s407, s409, s410, s413, s414, s430, s434, s453, s456, s473, s474, s475, s476, s477, s478, s479, s480, s481, s482, s483, s484, s485, s486, s487, s488, s489, s490, s491, s492, s493, s494, s495, s496, s497, s498, s499, s500, s501, s502, s503, s504, s505, s506, s507, s508, s509, s510, s511, s512, s513, s514, s515, s516, s517, s518, s519, s520, s521, s522, s523, s524, s525, s526, s527, s528, s529, s530, s531, s532, s533, s534, s535, s536, s537, s538, s539, s540, s541, s542, s543, s544, s545, s546, s547, s548, s549, s550, s551, s552, s553, s554, s556, s558, s561, s562, s564, s566, s568, s570, s580, s583, s594, s598, s608, s612, s619, s622, s630, s634, s640, s660, s661, s664, s690, s695, s698, s701, s705, s710, s711, s713, s716, s718, s730, s735, s737, s748, s750, s761, s763, s770}, 3: {s23, s25, s30, s36, s37, s40, s41, s48, s52, s53, s58, s60, s62, s69, s84, s85, s87, s134, s142, s144, s147, s149, s154, s339, s340, s359, s361, s384, s400, s420, s421, s422, s426, s428, s429, s436, s440, s450, s461, s579, s581, s584, s587, s591, s592, s602, s603, s606, s607, s616, s617, s618, s624, s626, s628, s637, s638, s656, s657, s672, s673, s674, s675, s678, s679, s688, s689, s691, s714, s715, s720, s722, s726, s771}, 4: {s51, s68, s73, s122, s130, s385, s401, s427, s432, s435, s441, s585, s588, s589, s590, s593, s595, s596, s597, s599, s600, s601, s610, s613, s614, s615, s625, s636, s643, s646, s676, s692, s693, s694, s696, s697, s704, s752, s755, s765, s768}, 5: {s26, s42, s65, s70, s74, s75, s97, s99, s107, s115, s116, s124, s126, s188, s190, s197, s206, s207, s210, s212, s245, s247, s268, s274, s276, s345, s346, s437, s567, s569, s620, s627, s629, s639, s644, s645, s666, s667, s699, s702, s724, s727, s728, s729, s732, s734, s739, s740, s741, s743, s746, s747, s753, s757, s759}, 6: {s132, s438, s582, s604, s605, s621, s632, s635, s647, s700, s703, s708, s709, s712, s742, s756, s767}, 7: {s117, s118, s136, s137, s215, s224, s226, s285, s293, s295, s302, s306, s307, s310, s312, s641, s706, s744, s745, s758, s760, s766, s772, s774, s775}, 8: {s642, s707, s769, s773}, 9: {s315, s325, s327}, 11: {s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, s17, s18, s19, s20, s21, s22, s31, s32, s34, s35, s39, s43, s44, s45, s46, s50, s55, s57, s59, s61, s63, s67, s72, s76, s77, s78, s79, s80, s81, s82, s83, s88, s89, s91, s92, s94, s96, s101, s102, s103, s106, s108, s109, s110, s111, s114, s119, s120, s123, s125, s127, s131, s135, s138, s139, s140, s141, s151, s152, s156, s177, s179, s181, s183, s185, s192, s199, s208, s209, s217, s227, s228, s233, s234, s236, s239, s241, s249, s270, s277, s279, s280, s282, s287, s296, s297, s304, s308, s309, s317, s328, s329, s333, s334, s335, s336, s337, s338, s341, s342, s343, s344, s347, s348, s349, s350, s351, s352, s353, s354, s355, s356, s357, s363, s364, s373, s374, s378, s382, s383, s399, s408, s411, s412, s415, s416, s417, s418, s419, s423, s424, s425, s431, s433, s439, s442, s443, s444, s445, s446, s448, s449, s451, s454, s457, s458, s459, s460, s462, s463, s464, s465, s466, s467, s468, s469, s470, s471, s472, s555, s557, s559, s560, s563, s565, s571, s572, s573, s574, s575, s576, s577, s578, s586, s609, s611, s623, s631, s633, s648, s649, s650, s651, s652, s653, s654, s655, s658, s659, s662, s663, s665, s668, s669, s670, s671, s677, s680, s681, s682, s683, s684, s685, s686, s687, s717, s719, s721, s723, s725, s731, s733, s736, s738, s749, s751, s754, s762, s764, s776, s777, s778, s779, s780} |
||||||||||
|
|
||||||||||