## rodin-b-sharp-user

 [Rodin-b-sharp-user] Detection of Cycles in a Graph From: Thiago Carvalho de Sousa - 2013-01-22 17:16:31 ```Dear all, I´m modelling a directed graph as a relation of a set to itself. "aa"," bb", "cc" and "dd" are nodes. So, I have: INVARIANTS nodes : pow(VERTEX_SET) graph : nodes <-> nodes INITIALISATION graph := {aa \mapsto bb, aa \mapsto cc, bb \mapsto dd, cc \mapsto dd, dd \mapsto aa, dd \mapsto bb} I´d like to detect cycles in this graph. Is there any simple way to check this? Maybe using ProB? Any suggestion? Thanks in advance, Thiago ```
 Re: [Rodin-b-sharp-user] Detection of Cycles in a Graph From: Alexei Iliasov - 2013-01-22 19:39:30 ```22.01.2013 17:16, Thiago Carvalho de Sousa пишет: > Dear all, > > I´m modelling a directed graph as a relation of a set to itself. > "aa"," bb", "cc" and "dd" are nodes. So, I have: > > INVARIANTS > nodes : pow(VERTEX_SET) > graph : nodes<-> nodes > > INITIALISATION > graph := {aa \mapsto bb, aa \mapsto cc, bb \mapsto dd, cc \mapsto dd, > dd \mapsto aa, dd \mapsto bb} > > I´d like to detect cycles in this graph. Is there any simple way to > check this? Maybe using ProB? Any suggestion? add theorem (or axiom if you rely on prob): not # z . z <: dom(graph) & {} <<: z & c <: graph[z] should be easy to check with prob or smt plugin > Thanks in advance, > > Thiago > > ------------------------------------------------------------------------------ > Master Visual Studio, SharePoint, SQL, ASP.NET, C# 2012, HTML5, CSS, > MVC, Windows 8 Apps, JavaScript and much more. Keep your skills current > with LearnDevNow - 3,200 step-by-step video tutorials by Microsoft > MVPs and experts. ON SALE this month only -- learn more at: > http://p.sf.net/sfu/learnnow-d2d > _______________________________________________ > Rodin-b-sharp-user mailing list > Rodin-b-sharp-user@... > https://lists.sourceforge.net/lists/listinfo/rodin-b-sharp-user ```