albertocasagrande / pymodelchecking Goto Github PK
View Code? Open in Web Editor NEWA Python model checking package
License: Other
pymodelchecking's People
Contributors
Stargazers
Watchers
Forkers
chdd mahameth gianricardo haitianwang teodorov bastianzim decadenza echentao transafeailab yuvalbir10pymodelchecking's Issues
The `modelcheck` function does not always return the same result
The modelcheck function does not always return the same value. For instance, the program
from pyModelChecking import *
from pyModelChecking.LTL import *
psi=A(And('one',X(And('two',X('three')))))
K = Kripke(R=[(0, 1), (1, 2), (2, 3), (3, 3)],
L={0: ['one'], 1: ['two'], 2: ['three']})
print(modelcheck(K, psi))
sometimes prints set() and sometimes {0}.
modelcheck results are not clear
hi,
im running simple traffic-light automaton and i'm not sure i understand the result.
with formula_a, i got empty set
but with formula_b, i got {1,2,3}
formula_a and formula_b are the same except of the order of the inner parts.
can you please help? is it my mistake?
from pyModelChecking.kripke import Kripke
from pyModelChecking.LTL import *
p = Parser()
K = Kripke(S=[1, 2, 3],
S0=[1],
R=[(1, 2), (2, 3), (3, 1)],
L={1: set(['green']),
2: set(['yellow']),
3: set(['red'])}
)
formula_a = 'A(G( (green or yellow or red) and not(green and yellow) and not(green and red) and not(red and yellow)))'
formula_b = 'A(G(not(green and yellow) and not(green and red) and not(red and yellow) and (green or yellow or red) ))'
res = modelcheck(K, formula_a)
print(res)
Publish the package on conda-forge
Publishing via conda-forge would be great contribution for the tool.
Test problem
Hello friend,
Could you please help me to test your project because i have some problems in language file,
can you give instructions to run model checking file.
Greeting,
Mohyiddine
RuntimeError when checking CTL formula
Hi,
Model checking A (true R p) produces a runtime error. Although this formula does not make sense (it should be equivalent to p), it is a valid CTL formula. The following piece of code shows the problem:
import pyModelChecking
from pyModelChecking.CTL.language import A, R, Bool, AtomicProposition
kripke = pyModelChecking.kripke.Kripke(
S = [0, 1],
S0 = {0},
R = [(0, 1), (1, 1)],
L = {0: set(), 1: set('p')}
)
formula = A(R(Bool(True), AtomicProposition('p')))
pyModelChecking.CTL.model_checking.modelcheck(kripke, formula)Its output is this:
Traceback (most recent call last):
File "example.py", line 13, in <module>
pyModelChecking.CTL.model_checking.modelcheck(kripke, formula)
File ".../pyModelChecking/CTL/model_checking.py", line 208, in modelcheck
return _checkStateFormula(kripke, formula, L=dict())
File ".../pyModelChecking/CTL/model_checking.py", line 158, in _checkStateFormula
Lalter_formula = _checkStateFormula(kripke, restr_f, L)
File ".../pyModelChecking/CTL/model_checking.py", line 126, in _checkStateFormula
return _checkNot(kripke, formula, L)
File ".../pyModelChecking/CTL/model_checking.py", line 40, in _checkNot
Lphi = _checkStateFormula(kripke, formula.subformula(0), L)
File ".../pyModelChecking/CTL/model_checking.py", line 151, in _checkStateFormula
return _checkEU(kripke, formula, L)
File ".../pyModelChecking/CTL/model_checking.py", line 99, in _checkEU
L[formula] = subgraph.get_reachable_set_from(Lphi[1])
File ".../pyModelChecking/graph.py", line 192, in get_reachable_set_from
for d in self.next(s):
File ".../pyModelChecking/graph.py", line 108, in next
raise RuntimeError('src = \'{}\' is not a node '.format(src) +
RuntimeError: src = '0' is not a node of (V=dict_keys([]), E=[])
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.