Why is x[“is_cyclic”] true for a single state?

[hklarner]

I am a bit confused with the results for the network irons_yeast. It shows that there is only one cyclic attractor, but the expression of the attractor is a steady state.

>>> import PyBoolNet
>>> primes = PyBoolNet.Repository.get_primes("irons_yeast")
>>> attrs = PyBoolNet.Attractors.compute_json(primes, "asynchronous", FnameJson="attrs.json")
Attractors.compute_json(..)
 Attractors.completeness(..) yes
 working on minimal trapspace 1/1: ------------------
  Attractors.univocality(..) yes
  Attractors.faithfulness(..) yes
  Attractors.find_attractor_state_by_randomwalk_and_ctl(..)
created attrs.json
>>> len(attrs["attractors"])
1
>>> x=attrs["attractors"][0]
>>> x["is_steady"]
False
>>> x["is_cyclic"]
True
>>> x["state"]
{'str': '010010000100011111', 'dict': {'CD': 0, 'CKI': 1, 'Cdc14': 0, 'Cdc20': 0, 'Cdh1': 1, 'Clb2': 0, 'Clb5': 0, 'Cln2': 0, 'Cln3': 0, 'FEAR': 1, 'MEN': 0, 'SFF': 0, 'SMBF': 0, 'Swi5': 1, 'Yhp1': 1, 'vB': 1, 'vM': 1, 'vS': 1}, 'prop': '!CD&CKI&!Cdc14&!Cdc20&Cdh1&!Clb2&!Clb5&!Cln2&!Cln3&FEAR&!MEN&!SFF&!SMBF&Swi5&Yhp1&vB&vM&vS'}

This network has 18 nodes and there are 18 bits in the expression '010010000100011111'. So I think this should be a steady state. But why it returns true for x[“is_cyclic”]?

Could you please help me to solve the problems? Thank you very much in advance.

[hklarner]

Very good point. The reason is that state is a single state that belongs to the attractor not the full list of states. Starting with this state you could explore all reachable states to compute the full list, if you want. But I am guessing that it will be a very long list. That's also the reason why I always return a single state. Enumerating attractor states in lists quickly becomes impossible. You could also compute the list with the accepting states that are returned by nusmv-a.

To see some successors:

primes = PyBoolNet.Repository.get_primes("irons_yeast")
attrs = PyBoolNet.Attractors.compute_json(primes, "asynchronous", FnameJson="irons_yeast_attrs.json")
state = attrs['attractors'][0]['state']['dict']
successors = PyBoolNet.StateTransitionGraphs.successors_asynchronous(primes, state)
print(s)

[{'CD': 0, 'CKI': 0, 'Cdc14': 1, 'Cdc20': 1, 'Cdh1': 1, 'Clb2': 0, 'Clb5': 0, 'Cln2': 0, 'Cln3': 1, 'FEAR': 1, 'MEN': 0, 'SFF': 1, 'SMBF': 0, 'Swi5': 1, 'Yhp1': 0, 'vB': 1, 'vM': 1, 'vS': 1},
{'CD': 1, 'CKI': 1, 'Cdc14': 1, 'Cdc20': 1, 'Cdh1': 1, 'Clb2': 0, 'Clb5': 0, 'Cln2': 0, 'Cln3': 1, 'FEAR': 1, 'MEN': 0, 'SFF': 1, 'SMBF': 0, 'Swi5': 1, 'Yhp1': 0, 'vB': 1, 'vM': 1, 'vS': 1}, 
{'CD': 1, 'CKI': 0, 'Cdc14': 0, 'Cdc20': 1, 'Cdh1': 1, 'Clb2': 0, 'Clb5': 0, 'Cln2': 0, 'Cln3': 1, 'FEAR': 1, 'MEN': 0, 'SFF': 1, 'SMBF': 0, 'Swi5': 1, 'Yhp1': 0, 'vB': 1, 'vM': 1, 'vS': 1}, 
{'CD': 1, 'CKI': 0, 'Cdc14': 1, 'Cdc20': 0, 'Cdh1': 1, 'Clb2': 0, 'Clb5': 0, 'Cln2': 0, 'Cln3': 1, 'FEAR': 1, 'MEN': 0, 'SFF': 1, 'SMBF': 0, 'Swi5': 1, 'Yhp1': 0, 'vB': 1, 'vM': 1, 'vS': 1}, 
{'CD': 1, 'CKI': 0, 'Cdc14': 1, 'Cdc20': 1, 'Cdh1': 1, 'Clb2': 0, 'Clb5': 0, 'Cln2': 0, 'Cln3': 1, 'FEAR': 1, 'MEN': 0, 'SFF': 0, 'SMBF': 0, 'Swi5': 1, 'Yhp1': 0, 'vB': 1, 'vM': 1, 'vS': 1}, 
{'CD': 1, 'CKI': 0, 'Cdc14': 1, 'Cdc20': 1, 'Cdh1': 1, 'Clb2': 0, 'Clb5': 0, 'Cln2': 0, 'Cln3': 1, 'FEAR': 1, 'MEN': 0, 'SFF': 1, 'SMBF': 1, 'Swi5': 1, 'Yhp1': 0, 'vB': 1, 'vM': 1, 'vS': 1}, 
{'CD': 1, 'CKI': 0, 'Cdc14': 1, 'Cdc20': 1, 'Cdh1': 1, 'Clb2': 0, 'Clb5': 0, 'Cln2': 0, 'Cln3': 1, 'FEAR': 1, 'MEN': 0, 'SFF': 1, 'SMBF': 0, 'Swi5': 1, 'Yhp1': 0, 'vB': 0, 'vM': 1, 'vS': 1}, 
{'CD': 1, 'CKI': 0, 'Cdc14': 1, 'Cdc20': 1, 'Cdh1': 1, 'Clb2': 0, 'Clb5': 0, 'Cln2': 0, 'Cln3': 1, 'FEAR': 1, 'MEN': 0, 'SFF': 1, 'SMBF': 0, 'Swi5': 1, 'Yhp1': 0, 'vB': 1, 'vM': 0, 'vS': 1}, 
{'CD': 1, 'CKI': 0, 'Cdc14': 1, 'Cdc20': 1, 'Cdh1': 1, 'Clb2': 0, 'Clb5': 0, 'Cln2': 0, 'Cln3': 1, 'FEAR': 1, 'MEN': 0, 'SFF': 1, 'SMBF': 0, 'Swi5': 1, 'Yhp1': 0, 'vB': 1, 'vM': 1, 'vS': 0}]

But the answer to your question is state is always a single is always a single state that is guaranteed to belong to the attractor, a representative