From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=unavailable autolearn_force=no version=3.4.4 X-Received: by 10.224.4.138 with SMTP id 10mr10721444qar.8.1377119987632; Wed, 21 Aug 2013 14:19:47 -0700 (PDT) X-Received: by 10.50.2.74 with SMTP id 10mr519531igs.15.1377119987591; Wed, 21 Aug 2013 14:19:47 -0700 (PDT) Path: eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!news.eternal-september.org!news.eternal-september.org!feeder.eternal-september.org!usenet.blueworldhosting.com!feeder02.blueworldhosting.com!npeer01.iad.highwinds-media.com!news.highwinds-media.com!feed-me.highwinds-media.com!q10no33550qai.0!news-out.google.com!c19ni456qak.0!nntp.google.com!fx3no3918427qab.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail Newsgroups: comp.lang.ada Date: Wed, 21 Aug 2013 14:19:47 -0700 (PDT) In-Reply-To: <87mwoastdi.fsf@nl106-137-194.student.uu.se> Complaints-To: groups-abuse@google.com Injection-Info: glegroupsg2000goo.googlegroups.com; posting-host=64.183.207.38; posting-account=zwxLlwoAAAChLBU7oraRzNDnqQYkYbpo NNTP-Posting-Host: 64.183.207.38 References: <87mwoastdi.fsf@nl106-137-194.student.uu.se> User-Agent: G2/1.0 MIME-Version: 1.0 Message-ID: <9d7e5c6c-aeb9-4ac1-a7b0-c048061ae4c6@googlegroups.com> Subject: Re: RTS graph and "temporal formulas" From: optikos@verizon.net Injection-Date: Wed, 21 Aug 2013 21:19:47 +0000 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable X-Received-Bytes: 6540 Xref: news.eternal-september.org comp.lang.ada:16925 Date: 2013-08-21T14:19:47-07:00 List-Id: On Wednesday, August 21, 2013 3:04:00 PM UTC-5, Emanuel Berg wrote: > I have an exam the 30th on RTS and there is one problem I cannot > solve, because there is nothing on this in the material, and the > teacher doesn't answer mails with questions. > > I turn to you You turn to the Ada-language Usenet group for a question about 1950s math= ematics-nomenclature? Oh well. Instead of "get off my lawn", I will point= you in the right direction, which generally leads away from here. :-) >, not to solve the problem, but to explain what it > means - once there, I hope to solve it myself. >=20 > The problem involves a graph. Apparently, your instructor is assuming that you already know Mealy finite-= state machines and their canonical notation (as opposed to Moore finite-sta= te machines). Most of your question is answered by http://en.wikipedia.org= /wiki/Mealy_machine (as opposed to http://en.wikipedia.org/wiki/Moore_machi= ne, which utilizes the same stimulus/response notation but on the states=3D= vertexes instead of on the transitions=3Dedges). I will utilize the initia= lism FSA (for finite-state automaton) below. > - there are states: circles with names (e.g., "B") and conditions > (x <=3D 10) (sometimes, the states do not have conditions) > - one state has a double circle: is this the initial state? yes. If there were a terminal state, it would be solid black, instead of = white with a black perimeter. > - there are edges Here you are utilizing graph-theoretic terminology. Edges are known as t= ransitions in Mealy & Moore FSAs (and depending on context, either transiti= ons or arcs in Petri networks). > between the states Here you revert to Mealy & Moore FSA terminology. States are known as ve= rtexes or vertices in graph-theoretic terminology. > , that are directed All transitions in Mealy & Moore FSAs are directed. There is only traver= sal as "go to" running forward in time, not untraversal as "come from" runn= ing backward in time. > : those > edges are tagged: sometimes with conditions (x < 5) In Mealy's FSA notation, each edge may be labeled by a stimulus/response.= [Note the slash; it is part of the notation.] The Mealy FSA stays in its = current state v until one of the transitions egressing v has a stimulus-con= straint that matches an actual stimulus in the FSA's environmental context.= Hence, your "condition" is a stimulus. > , sometimes >=20 > with assignments (x :=3D 0) And your "assignment" is a response actualized by traversing that transit= ion e, proceeding to the state into e ingresses. > , and sometimes with both (y < 0 and y >=20 > :=3D 0) Your professor should have his hand smacked for abuse of notation firmly = established in the 1950s and still widely utilized in electrical engineerin= g (and deriving from Petri nets in chemical-manufacturing plants in the 193= 0s). Your professor's logical comparisons are Mealy's "leftward of the sla= sh" for stimulus. Your professor's ":=3D" is Mealy's "rightward of the sla= sh" for response. Apparently your professor's exposure to FSAs is 2nd hand= from C-language source-code in imperative-instruction sequential software,= not from seminal references in the 1950s (or the 1930s). > - the variables (x and y are "clocks") Progress of monotonically-increasing measured realtime is merely yet anot= her "sensor" from which the Mealy FSA is hooked up to the contextual enviro= nment to receive stimuli (much as your brain acquires stimuli from its five= senses as sensors). [In electrical engineering, often the sensors are mer= ely digital-logic lines.] Out of the potentially vast avalanche of incomin= g stimuli from the sensors, only the stimulus-constraints that are actionab= le (to progress to a different state and/or to evoke a response) at each pa= rticular transition egressing from each state (when it is the current state= ) are overtly stated. When the multitude of stimulus-constraints are not a= ctionable, that multitude is unmentioned at that transition. Likewise, out= of the multitude of responses not effected by a transition, that multitude= is unmentioned at that transition. > What does it all mean? It means either that you are missing a prerequisite for this class or (if= this is the course of first exposure to FSAs and their brethren) that your= professor has failed to introduce you to Mealy FSAs, Moore FSAs, Petri net= s, Viterbi dynamic-programming algorithm, and Markov chains. (Only the fir= st of these 5 related concepts is utilized in Problem 7, but you should, at= your leisure, study the other 4 sometime too.) > Check out the graph here: > http://user.it.uu.se/~embe8573/2011.pdf > (Problem 7, the last one.) > They also mention "temporal formulas" to describe properties of > the system, that the graph is a model of. Do you know of a > resource, that describes the syntax and semantics of such > formulas? Formulae from temporal logic: https://en.wikipedia.org/wiki/Temporal_logi= c a branch of symbolic logic: https://en.wikipedia.org/wiki/Symbolic_logic > Thanks :) >=20 >=20 >=20 > --=20 >=20 > Emanuel Berg - programmer (hire me! CV below) > computer projects: http://user.it.uu.se/~embe8573 > internet activity: http://home.student.uu.se/embe8573